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