proposition: Lemma ring_mul_0_r : forall x, x * 0 == 0.
proof: Proof. intro x; setoid_replace (x*0) with (x*(0+1) + -x). - rewrite ring_add_0_l ; rewrite ring_mul_1_r . rewrite ring_opp_def ; fold zero; reflexivity. - rewrite ring_distr_r ;rewrite ring_mul_1_r . 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