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