proposition: Theorem rng_mul_nat_assoc : ∀ α (R : ring α) n a b, (rng_mul_nat R n a * b = rng_mul_nat R n (a * b))%K.
proof: Proof. intros α R n a b. induction n; simpl. rewrite rng_mul_0_l; reflexivity. rewrite rng_mul_add_distr_r, IHn; reflexivity. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn