proposition: Lemma add_mult_dev_ok : forall P rP fv n lm, add_mult_dev rP P fv n lm == rP + P@fv*pow_N rI rmul (hd fv) n * r_list_pow lm.
proof: Proof. intros P; induction P as [|p P IHP|P2 IHP1 p P3 IHP2];simpl;intros rP fv n lm. - rewrite mkadd_mult_ok. rewrite add_pow_list_ok; Esimpl. - rewrite IHP. simpl. rewrite add_pow_list_ok; Esimpl. - change (match P3 with | Pc c => c ?=! cO | Pinj _ _ => false | PX _ _ _ => false end) with (Peq P3 P0). change match n with | N0 => Npos p | Npos q => Npos (p + q) end with (N.add (Npos p) n);trivial. assert (H := Peq_ok P3 P0). destruct (P3 ?== P0). + rewrite (H eq_refl). rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl. add_permut. mul_permut. + rewrite IHP2. rewrite IHP1. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl. add_permut. mul_permut. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory