proposition: Theorem is_zero_diff: forall x y, (x - y) ?0 = true -> x = y.
proof: Proof. intros x y H. apply trans_equal with (y + (x - y)); try ring. case (Eth.(is_zero_correct) (x - y)); intros H1 H2; rewrite H1; auto; ring. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith