proposition: Theorem Keq_opp_is_zero: forall x, x = - x -> x = 0.
proof: Proof. intros x H. case (@Kmult_integral (1+1:K) x); simpl; auto. apply trans_equal with (x + x); simpl; try ring. pattern x at 1; rewrite H; ring. intros H1; case two_not_zero; auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith