proposition: Lemma inversible_mult_inv: forall x y, [x ** y] -> [x] /\ [y].
proof: Proof. assert (F1 := N_lt_2). intros x y (z, Hz); split. exists (y * z)%Z; rewrite <- Hz. unfold nmul. rewrite Zmodml; auto with zarith. rewrite Zmult_assoc; auto. exists (x * z)%Z; rewrite <- Hz. unfold nmul. rewrite Zmodml; auto with zarith. rewrite Zmult_assoc; auto. rewrite (Zmult_comm x); auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod