proposition: Lemma mkmult_c_ok : forall c lm, mkmult_c c lm == [c] * r_list_pow lm.
proof: Proof. intros c lm;unfold mkmult_c;simpl. case_eq (get_sign c);intros c0; try intros H. - assert (H1 := (morph_eq CRmorph) c0 cI). destruct (c0 ?=! cI). + rewrite (morph_eq CRmorph _ _ (sign_spec get_sign_spec _ H)). Esimpl. rewrite H1;trivial. rewrite <- r_list_pow_rev;trivial;Esimpl. apply mkmultm1_ok. + rewrite <- r_list_pow_rev; apply mkmult_rec_ok. - apply mkmult_c_pos_ok. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory