proposition: Lemma freeg_ind_dom (R : ringType) (K : choiceType) (F : pred K): forall (P : {freeg K / R} -> Prop), (forall D : {freeg K / R}, [predI dom (G:=R) (K:=K) D & [predC F]] =1 pred0 -> P D) -> (forall (k : R) (x : K) (D : {freeg K / R}), x \notin dom (G:=R) (K:=K) D -> k != 0 -> ~~ F x -> P D -> P (<< k *g x >> + D)) -> forall D : {freeg K / R}, P D.
proof: Proof. by move=> P; apply/(@freeg_rect_dom R K F P). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)