proposition: Lemma Zind : forall (P : Z -> Prop) (p : Z), P p -> (forall q : Z, (p <= q)%Z -> P q -> P (q + 1)%Z) -> forall q : Z, (p <= q)%Z -> P q.
proof: Proof. intros P p. intro. intro. cut (forall q : Z, (p <= q)%Z -> exists k : nat, q = (p + k)%Z). intro. cut (forall k : nat, P (p + k)%Z). intro. intros. cut (exists k : nat, q = (p + Z_of_nat k)%Z). intro. case H4. intros. rewrite H5. apply H2. apply H1. assumption. intro. induction k as [| k Hreck]. simpl in |- *. ring_simplify (p + 0)%Z. assumption. replace (p + Z_of_nat (S k))%Z with (p + k + 1)%Z. apply H0. apply Zplus_le_reg_l with (p := (- p)%Z). replace (- p + p)%Z with (Z_of_nat 0). ring_simplify (- p + (p + Z_of_nat k))%Z. apply Znat.inj_le. apply Nat.le_0_l. ring_simplify; auto with arith. assumption. rewrite (Znat.inj_S k). unfold Z.succ in |- *. ring. intros. cut (exists k : nat, (q - p)%Z = Z_of_nat k). intro. case H2. intro k. intros. exists k. apply Zplus_reg_l with (n := (- p)%Z). replace (- p + q)%Z with (q - p)%Z. rewrite H3. ring. ring. apply Z_of_nat_complete. unfold Zminus in |- *. apply Zle_left. assumption. Qed.
imports: Coq(Lia)