proposition: Lemma leR_trans x y z : x <= y -> y <= z -> x <= z.
proof: Proof. by move=> le_xy le_yz a /le_yz/le_xy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq order) mathcomp(ssralg ssrnum ssrint rat) fourcolor(real) Coq(Setoid Morphisms)