proposition: Theorem ident_l_unique : forall x y, x * y = y -> x = ident.
proof: Proof. intuition. rewrite <- (group_cyclic g x). rewrite <- (@groupIdent _ groupOp ident _ G _ _ _ FCG g). eapply groupExp_eq_if; trivial. apply g_generator. rewrite <- (group_cyclic g y) in H; eauto. rewrite <- (group_cyclic g x) in H; eauto. rewrite <- groupExp_plus in H. apply groupExp_eq in H; trivial. eapply modNat_add_same_r. eauto. apply g_generator. apply g_generator. apply g_generator. apply g_generator. apply g_generator. Qed.
imports: FCF.Rat FCF.StdNat