proposition: Lemma Zlt_lower_bound_ind : forall P:Z -> Prop, 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 ? x ?; now apply Zlt_lower_bound_rec with z. Qed.
imports: BinInt Zcompare Zorder Znat Zmisc Wf_nat