proposition: Lemma unsat_consider ij th : wf_consider ij th -> unsat (AddClause th (& ? in ij)) -> unsat th.
proof: Proof. case: ij => i j; case/andP; set sym_t := sub_match _ _ => lti ltj Uthij m m_th. wlog le_m21: m m_th / sym_t -> (m.2 <= m.1)%N. move=> IH; apply: (IH m m_th) => sym_th. rewrite leqNgt; apply/negP=> /leqW le_m1_m2. by have /(sat_exact sym_th)/IH[] := sat_tr m_th. apply: (Uthij m); congr (_ && _): (m_th) => /=; case: (th_bbox th) => ri rj /=. have [[odd_m1 _ m1gt1 m2gt1 neq_m12] _ _] := LmodelP m. rewrite /sub_bbox !geq_max (leq_trans ltj) ?(leq_trans lti) //; case: orP => //. rewrite -(ltnS 4) (odd_geq _ odd_m1) ltnS. case=> [/leq_trans-> // | /le_m21]; first by have [/andP[]] := and3P m_th. by rewrite leq_eqVlt eq_sym (negPf neq_m12); apply: leq_trans. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg matrix poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor center gproduct cyclic pgroup abelian frobenius) mathcomp(mxalgebra mxrepresentation vector falgebra fieldext galois) mathcomp(ssrnum rat algC algnum classfun character) mathcomp(integral_char inertia vcharacter) odd_order(PFsection1 PFsection2)