proposition: Theorem lt_neq : ∀ n m, n < m → not (qeq n m).
proof: Proof. intros n m Hlt. intros H. destruct n as [n| ]. destruct m as [m| ]; [ idtac | inversion H ]. apply qfin_lt_mono in Hlt. apply qfin_inj in H. rewrite H in Hlt. revert Hlt; apply Qlt_irrefl. destruct m as [m| ]; [ inversion H | inversion Hlt ]. Qed.
imports: Utf8 QArith Misc