proposition: Lemma Qlt_transitive : forall x y z : Q, Qlt x y -> Qlt y z -> Qlt x z.
proof: Proof. intros x y z H1 H2. unfold Qlt in |- *. apply Qgt_trans with y; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)