proposition: Lemma inversible_1: forall n, 1 < n -> inversible n 1.
proof: Proof. intros n Hn; exists 1%Z; rewrite Zmult_1_r; apply Zmod_small; split; auto with zarith. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod