proposition: Lemma eunitgenlawl : forall x : E, Equal (genlaw e x) x.
proof: Proof. intros x; try assumption. apply Trans with (genlaw (genlaw x (geninv x)) x); auto with algebra. apply Trans with (genlaw x (genlaw (geninv x) x)); auto with algebra. apply Trans with (genlaw x e); auto with algebra. Qed.
imports: Sub_group Abelian_group_cat