proposition: Lemma unsat_fill ij th : let fill_cl cl := if (th_dim th).+1 %/ 1 is k.+1 then let: Wrap thk := ext_cl th cl k 1 in wf_fill k cl.2 /\ unsat thk else True in oapp fill_cl False (get_cl ij th) -> unsat th.
proof: Proof. rewrite divn1; case: get_clP => //= cl [th_cl _]. case Dthk: ext_cl => [th1] [wf_thk Uth1] m m_th. by have [mk] := sat_fill m_th th_cl wf_thk; rewrite Dthk => /Uth1. 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)