proposition: Lemma Qlt_le_trans : forall x y z : Q, Qlt x y -> Qle y z -> Qlt x z.
proof: Proof. intros [| x| x] [| y| y] [| z| z] Hxy Hyz; trivial; try QltCleanAbsurdCases; case (Qle_lt_eq_dec _ _ Hyz); intro Hyz'; [ apply Qlt_transitive with (Qpos y) | rewrite <- Hyz' | apply Qlt_transitive with (Qneg y) | rewrite <- Hyz' ]; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)