proposition: Lemma mkmult_c_pos_ok : forall c lm, mkmult_c_pos c lm == [c]* r_list_pow lm.
proof: Proof. intros c lm;unfold mkmult_c_pos;simpl. assert (H := (morph_eq CRmorph) c cI). rewrite <- r_list_pow_rev; destruct (c ?=! cI). - rewrite H;trivial;Esimpl. apply mkmult1_ok. - apply mkmult_rec_ok. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory