proposition: Theorem Zlt_bool_spec : forall x y, Zlt_bool_prop x y (Zlt_bool x y).
proof: Proof. intros x y. generalize (Zlt_is_lt_bool x y). case Zlt_bool ; intros (H1, H2) ; constructor. now apply H2. destruct (Zle_or_lt y x) as [H|H]. exact H. now specialize (H1 H). Qed.
imports: Coq(ZArith Lia Zquot)