proposition: Theorem same_e_for_H_and_G: H.(e) = G.(e).
proof: Proof. apply trans_equal with (op H.(e) H.(e)); sauto. apply trans_equal with (op H.(e) (op G.(e) (H.(i) G.(e)))); sauto. eq_tac; sauto. apply trans_equal with (op G.(e) (op G.(e) (H.(i) G.(e)))); sauto. repeat rewrite H.(assoc); sauto. eq_tac; sauto. apply trans_equal with G.(e); sauto. apply trans_equal with (op G.(e) H.(e)); sauto. eq_tac; sauto. Qed.
imports: List UList ListAux ZArith Znumtheory NatAux FGroup