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