(n:nat)(Q n)==(n:nat)(P (inject_nat n)) ===> (x:Z)`x > 0) -> (P x) /\ || || (Q O) (n:nat)(Q n)->(Q (S n)) <=== (P 0) (x:Z) (P x) -> (P (Zs x)) <=== (inject_nat (S n))=(Zs (inject_nat n)) <=== inject_nat_completeThen the diagram will be closed and the theorem proved.