proposition: Lemma inversible_mult: forall a b, [a] -> [b] -> [a ** b].
proof: Proof. assert (F1 := N_lt_2). intros a b (z1, H1) (z2, H2). exists (z1 * z2)%Z. unfold nmul. rewrite Zmodml; auto with zarith. replace (a * b * (z1 * z2))%Z with ((a * z1) * (b * z2))%Z; try ring. rewrite Zmult_mod; auto with zarith. rewrite H1; rewrite H2; rewrite Zmod_small; auto with zarith. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod