@@ -77,3 +77,10 @@ multInverseInversesR l r =
7777 let step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (l <.> inverse r)) step4 in
7878 let step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5 in
7979 replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6
80+
81+multNegativeByNegativeIsPositive : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> inverse r = l <.> r
82+multNegativeByNegativeIsPositive l r =
83+ rewrite multInverseInversesR (inverse l) r in
84+ rewrite sym $ multInverseInversesL (inverse l) r in
85+ rewrite inverseSquaredIsIdentity l in
86+ Refl