proposition: Lemma mon_of_pol_ok : forall P m, mon_of_pol P = Some m -> forall l, [fst m] * Mphi l (snd m) == P@l.
proof: Proof. intros P; induction P as [c|p P IHP|P2 IHP1 ? P3 ?];simpl;intros m H l;Esimpl. - assert (H1 := (morph_eq CRmorph) c cO). destruct (c ?=! cO). + discriminate. + inversion H;trivial;Esimpl. - generalize H;clear H;case_eq (mon_of_pol P). + intros (c1,P2) H0 H1; inversion H1; Esimpl. generalize (IHP (c1, P2) H0 (jump p l)). rewrite mkZmon_ok;simpl;auto. + intros; discriminate. - generalize H;clear H;change match P3 with | Pc c => c ?=! cO | Pinj _ _ => false | PX _ _ _ => false end with (P3 ?== P0). assert (H := Peq_ok P3 P0). destruct (P3 ?== P0). + case_eq (mon_of_pol P2);try intros (cc, pp); intros H0 H1. * inversion H1. simpl. rewrite mkVmon_ok;simpl. rewrite H;trivial;Esimpl. generalize (IHP1 _ H0); simpl; intros HH; rewrite HH; rsimpl. * discriminate. + intros;discriminate. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory