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