proposition: Lemma subsetC_P A B E : sub A E -> sub B E -> (sub A (E -s B) <-> sub B (E -s A)).
proof: Proof. move => aE bE;split => i1 t ts;apply/setC_P; split. - by apply bE. - by move /i1 => /setC_P; case. - by apply aE. - by move /i1 => /setC_P; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)