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