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