proposition: Lemma properU2_r A B : ~(sub A B) <-> ssub B (A \cup B).
proof: Proof. split. move => nba; split; [ apply:subsetU2r | dneg hh ;by apply /setU2id_Pl]. by move => [_ hb] /setU2id_Pl h; case: hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)