proposition: Lemma mult_dev_ok : forall P fv n lm, mult_dev P fv n lm == 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 fv n lm;Esimpl. - rewrite mkmult_c_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. mul_permut. + rewrite add_mult_dev_ok. rewrite IHP1; rewrite add_pow_list_ok. destruct n;simpl;Esimpl;rewrite pow_pos_add;Esimpl. add_permut; mul_permut. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory