proposition: Lemma ltc_trans x a b : x < a -> (a < b)%R -> x < b.
proof: Proof. by case: x a b => x []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)