proposition: Lemma commringfracl1 (X : commring) (x1 x2 x3 x4 a1 a2 s1 s2 s3 s4 : X) (eq1 : paths ((x1 * s2) * a1) ((x2 * s1) * a1)) (eq2 : paths ((x3 * s4) * a2) ((x4 * s3) * a2)) : paths ((((s3 * x1) + (s1 * x3)) * (s2 * s4)) * (a1 * a2)) ((((s4 * x2) + (s2 * x4)) * (s1 * s3)) * (a1 * a2)).
proof: 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 : paths (((s3 * x1) * (s2 * s4)) * (a1 * a2)) (((s4 * x2) * (s1 * s3)) * (a1 * a2))). { destruct (assoc2 (s3 * x1) s2 s4). rewrite (assoc2 s3 x1 s2). rewrite (rer (s3 * (x1 * s2)) s4 a1 a2). rewrite (assoc2 s3 (x1 * s2) a1). destruct (assoc2 (s4 * x2) s1 s3). rewrite (assoc2 s4 x2 s1). rewrite (rer (s4 * (x2 * s1)) s3 a1 a2). rewrite (assoc2 s4 (x2 * s1) a1). destruct 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 : paths (((s1 * x3) * (s2 * s4)) * (a1 * a2)) (((s2 * x4) * (s1 * s3)) * (a1 * a2))). { destruct (comm2 s4 s2). destruct (comm2 s3 s1). destruct (comm2 a2 a1). destruct (assoc2 (s1 * x3) s4 s2). destruct (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). destruct eq2. destruct (comm2 ((x3 * s4) * a2) s1). destruct (comm2 ((x3 *s4) * a2) s2). rewrite (rer ((x3 * s4) * a2) s1 s2 a1). apply idpath. } destruct e1. destruct e2. apply idpath. Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids