proposition: Lemma ssub_trans2 b a c: sub a b -> ssub b c -> ssub a c.
proof: Proof. move => sab [sbc nbc]; split; first by apply: (sub_trans sab). by dneg ac;apply: (extensionality sbc); rewrite -ac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)