proposition: Lemma Zlt_lower_bound_rec : forall P:Z -> Type, forall z:Z, (forall x:Z, (forall y:Z, z <= y < x -> P y) -> z <= x -> P x) -> forall x:Z, z <= x -> P x.
proof: Proof. intros P z Hrec x Hx. rewrite <- (Z.sub_simpl_r x z). apply Z.le_0_sub in Hx. pattern (x - z); apply Zlt_0_rec; trivial. clear x Hx. intros x IH Hx. apply Hrec. - intros y (Hy,Hy'). rewrite <- (Z.sub_simpl_r y z). apply IH; split. + now rewrite Z.le_0_sub. + now apply Z.lt_sub_lt_add_r. - now rewrite <- (Z.add_le_mono_r 0 x z). Qed.
imports: BinInt Zcompare Zorder Znat Zmisc Wf_nat