proposition: Lemma inversible_is_zero: forall x, [x] -> pis_zero (x :%p) = false.
proof: Proof. intros x1 H1. case (pis_zero_correct (to_p x1)); case pis_zero; auto. intros HH _; generalize (HH (refl_equal true)); clear HH; intros HH. case (@inversible_is_not_k0 x1); auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod