proposition: Lemma set_lt_leT a b c: a <s b -> b <=s c -> a <s c.
proof: Proof. move => [le1 ne] le2; move:(set_leT le1 le2) => le3. split; [ exact | dneg eq1]. exact: (EqT eq1 (set_leA (set_le_i1 le1 eq1) le2)). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)