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