proposition: Lemma set_le_i2 a b c: a <=s b -> b \Eq c -> a <=s c.
proof: Proof. move => [f [fb sf tf]] [g [[bg _] sg tg]]. exists (g \co f);saw; apply: compose_fi => //; split; (try fct_tac); ue. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)