proposition: Lemma ring_opp_zero : -0 == 0.
proof: Proof. rewrite <- (ring_mul_0_r 0). rewrite ring_opp_mul_l. repeat rewrite ring_mul_0_r. reflexivity. Qed.
imports: Setoid BinPos BinNat Morphisms Setoid Bool ZArith_base Algebra_syntax