proposition: Theorem eq_1_0_all_0 : (1 = 0)%K → ∀ a, (a = 0)%K.
proof: Proof. intros H a. rewrite <- rng_mul_1_l. rewrite H, rng_mul_0_l. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m