proposition: Theorem Keq_minus_eq: forall x y, x - y = 0 -> x = y.
proof: Proof. intros x y H. apply trans_equal with (y + (x - y)); try ring. rewrite H; ring. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith