Lemma commringfracl1 (X : commring) (x1 x2 x3 x4 a1 a2 s1 s2 s3 s4 : X) (eq1 : (x1 * s2) * a1 = (x2 * s1) * a1) (eq2 : (x3 * s4) * a2 = (x4 * s3) * a2) : ((s3 * x1 + s1 * x3) * (s2 * s4)) * (a1 * a2) = ((s4 * x2 + s2 * x4) * (s1 * s3)) * (a1 * a2). Proof. intros. set (rdistr := ringrdistr X). set (assoc2 := ringassoc2 X). set (op2axs := commringop2axs X). set (comm2 := ringcomm2 X). set (rer := abmonoidoprer op2axs). rewrite (rdistr (s3 * x1) (s1 * x3) (s2 * s4)). rewrite (rdistr (s4 * x2) (s2 * x4) (s1 * s3)). rewrite (rdistr ((s3 * x1) * (s2 * s4)) ((s1 * x3) * (s2 * s4)) (a1 * a2)). rewrite (rdistr ((s4 * x2) * (s1 * s3)) ((s2 * x4) * (s1 * s3)) (a1 * a2)). clear rdistr. assert (e1 : ((s3 * x1) * (s2 * s4)) * (a1 * a2) = ((s4 * x2) * (s1 * s3)) * (a1 * a2)). { induction (assoc2 (s3 * x1) s2 s4). rewrite (assoc2 s3 x1 s2). rewrite (rer (s3 * (x1 * s2)) s4 a1 a2). rewrite (assoc2 s3 (x1 * s2) a1). induction (assoc2 (s4 * x2) s1 s3). rewrite (assoc2 s4 x2 s1). rewrite (rer (s4 * (x2 * s1)) s3 a1 a2). rewrite (assoc2 s4 (x2 * s1) a1). induction eq1. rewrite (comm2 s3 ((x1 * s2) * a1)). rewrite (comm2 s4 ((x1 * s2) * a1)). rewrite (rer ((x1 * s2) * a1) s3 s4 a2). apply idpath. } assert (e2 : ((s1 * x3) * (s2 * s4)) * (a1 * a2) = ((s2 * x4) * (s1 * s3)) * (a1 * a2)). { induction (comm2 s4 s2). induction (comm2 s3 s1). induction (comm2 a2 a1). induction (assoc2 (s1 * x3) s4 s2). induction (assoc2 (s2 * x4) s3 s1). rewrite (assoc2 s1 x3 s4). rewrite (assoc2 s2 x4 s3). rewrite (rer (s1 * (x3 * s4)) s2 a2 a1). rewrite (rer (s2 * (x4 * s3)) s1 a2 a1). rewrite (assoc2 s1 (x3 * s4) a2). rewrite (assoc2 s2 (x4 * s3) a2). induction eq2. induction (comm2 ((x3 * s4) * a2) s1). induction (comm2 ((x3 *s4) * a2) s2). rewrite (rer ((x3 * s4) * a2) s1 s2 a1). apply idpath. } induction e1. induction e2. apply idpath. Qed.
Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.MoreFoundations.Orders.