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