proposition: Lemma Qlt_leneq: forall p q : Q, p < q <-> p <= q /\ ~ (p == q).
proof: Proof. intros p q; split; intros H. - rewrite Qlt_alt in H; rewrite Qle_alt, Qeq_alt. rewrite H; split; intros H1; inversion H1. - rewrite Qlt_alt; rewrite Qle_alt, Qeq_alt in H. destruct (p ?= q); tauto. Qed.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool