proposition: Lemma nat_to_group_minus : forall n m : nat, n > m -> Equal (nat_to_group (n - m)) (sgroup_law G (nat_to_group n) (group_inverse G (nat_to_group m))).
proof: Proof. intros n m H'; try assumption. replace n with (m + (n - m)). rewrite minus_plus. apply Trans with (sgroup_law G (sgroup_law G (nat_to_group m) (nat_to_group (n - m))) (group_inverse G (nat_to_group m))); auto with *. apply GROUP_reg_right with (nat_to_group m); auto with *. apply Trans with (sgroup_law G (sgroup_law G (nat_to_group m) (nat_to_group (n - m))) (sgroup_law G (group_inverse G (nat_to_group m)) (nat_to_group m))); auto with *. apply Trans with (sgroup_law G (sgroup_law G (nat_to_group m) (nat_to_group (n - m))) (monoid_unit G)); auto with *. apply Trans with (sgroup_law G (nat_to_group m) (nat_to_group (n - m))); auto with *. auto with *. Qed.
imports: Zring Group_kernel