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