proposition: Lemma canonical_mults : forall m l, ~ zeroP (A:=A) A0 eqA (n:=n) m -> canonical A0 eqA ltM l -> canonical A0 eqA ltM (mults m l).
proof: Proof. Proof using plusA os minusA invA eqA_dec divA cs A1. intros m l; elim l; simpl in |- *; auto. intros a l0 H' H'0 H'1. apply mults_order_l; auto. Qed.