proposition: Theorem is_zero_true: forall e, is_zero e = true -> e = 0.
proof: Proof. intro e; generalize (Eth.(is_zero_correct) e); case is_zero; auto; intros (H,_); auto. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith