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