proposition: Lemma sat_fill m th cl (k := th_dim th) : sat m th -> cl \in th -> wf_fill k cl.2 -> exists mr : {CFk | is_Rmodel CFk}, sat (Model (LmodelP m) (svalP mr)) (unwrap (ext_cl th cl k 1)).
proof: Proof. move=> m_th th_cl /andP[/eqP sz_kvs n3cl]. wlog sz_m: m m_th / size m = k. have lekm: (k <= size m)%N by have [] := and3P m_th. have mrP: is_Rmodel (take k m). have [] := RmodelP m; rewrite -{1 2}(cat_take_drop k m) orthonormal_cat /=. by case/andP=> o1mr _ /allP; rewrite all_cat => /andP[/allP]. move/(_ (Model (LmodelP m) mrP)); apply; rewrite ?size_takel //. congr (_ && _): m_th; rewrite lekm size_takel ?leqnn //=. apply: eq_in_all => cl1 /th_dimP lt_cl1; congr (_ && _). by apply: eq_in_all => kv1 /lt_cl1 lt_kv1; rewrite /sat_lit nth_take ?lt_kv1. have [_ _ [//||dk cl_dk o_dk_m]] := norm_clP m_th th_cl. by rewrite sz_kvs sz_m. have CFkP: is_Rmodel (rcons m (dchi dk)). have [o1m /allP Zm] := RmodelP m. split; last by apply/allP; rewrite all_rcons /= dchi_vchar. rewrite -cats1 orthonormal_cat o1m orthogonal_sym o_dk_m. by rewrite /orthonormal /= cfnorm_dchi eqxx. exists (exist _ _ CFkP); set mk := Model _ _. have{m_th} mk_th: sat mk th. congr (_ && _): m_th; rewrite size_rcons sz_m leqnn ltnW //=. apply: eq_in_all => cl1 /th_dimP lt_cl1; congr (_ && _). apply: eq_in_all => kv1 /lt_cl1 lt_kv1; congr ('[_, _] == _). by rewrite nth_rcons sz_m lt_kv1. have [|{mk_th}v ub_v m_th] := sat_cases k mk_th th_cl. rewrite /wf_ext_cl size_rcons sz_m (contraFN _ (ltnn k)) //=. by case/mapP=> kv kv_cl {1}->; rewrite (th_dimP _ _ th_cl). suffices: 0 < v by case/or4P: ub_v m_th => // /eqP->. case: (ext_clP k v th_cl) m_th => th1 -> [th1_cl1 _] /and3P[_ _]. case/allP/(_ _ th1_cl1)/and3P=> _ /eqP/=. by rewrite nth_rcons sz_m ltnn eqxx CintrE => <- _; rewrite -dirr_consttE. 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)