proposition: Lemma set_le_ltT a b c: a <=s b -> b <s c -> a <s c.
proof: Proof. move => le1 [le2 bc]; move:(set_leT le1 le2) => le3. split; [ exact | move/EqS => eq1; case bc]. exact:(EqT (set_leA (set_le_i2 le2 eq1) le1) (EqS eq1)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)