proposition: Lemma lt_gec_trans a b x : (a < b)%R -> x >= b -> x >= a.
proof: Proof. by move/ltW; apply: le_gec_trans. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)