proposition: Theorem rng_mul_nat_add_distr_r : ∀ α (r : ring α) a m n, (rng_mul_nat r (m + n) a = rng_mul_nat r m a + rng_mul_nat r n a)%K.
proof: Proof. intros α r a m n. revert a n. induction m; intros; simpl. rewrite rng_add_0_l; reflexivity. rewrite IHm. apply rng_add_shuffle0. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn