proposition: Lemma ring_mul_0_l : forall x, 0 * x == 0.
proof: Proof. intro x. setoid_replace (0*x) with ((0+1)*x + -x). - rewrite ring_add_0_l. rewrite ring_mul_1_l . rewrite ring_opp_def . fold zero. reflexivity. - rewrite ring_distr_l . rewrite ring_mul_1_l . rewrite <- ring_add_assoc ; rewrite ring_opp_def . rewrite ring_add_comm ; rewrite ring_add_0_l ;reflexivity. Qed.
imports: Setoid BinPos BinNat Morphisms Setoid Bool ZArith_base Algebra_syntax