proposition: Lemma cnf_sum_monP x y d: (forall p, inc p (cnf_sum_mons x y d) <-> cnf_sum_monp x y d p).
proof: Proof. split. case/setU2_P. by case/setU2_P => /Zo_P [ha hb] ; [ constructor 1 | constructor 2]. by move => /set1_P; constructor 3. case => h. - by apply: setU2_1; apply: setU2_1; apply/Zo_P. - by apply: setU2_1; apply: setU2_2; apply/Zo_P. - apply: setU2_2; rewrite - h; apply: set1_1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)