proposition: Lemma inversible_kO: forall z1 z2, z2 = 0 -> z1:%p = z2 -> [z1] -> False.
proof: Proof. intros z1 z2 H1 H2 H3. generalize (inversible_is_not_k0 H3). rewrite H2; rewrite H1. intros H; case H; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod