fix ifFlip breaking changes

Author: odderwiser

lib/Haskell/Law/Ord/Int.agda

@@ -108,20 +108,28 @@ instance
 
   iLawfulOrdInt .min2if a@(int64 x) b@(int64 y)
     with isNegativeInt a in h₁ | isNegativeInt b in h₂ 
-  ...| True  | True rewrite lte2ngt x y 
-    | sym $ ifFlip (y < x) b a  = eqReflexivity (if (y < x) then b else a)
+  ...| True  | True 
+    rewrite lte2ngt x y 
+    | ifFlip (y < x) a b 
+    = eqReflexivity (if (y < x) then b else a)
   ...| True  | False = eqReflexivity x
   ...| False | True rewrite eqSymmetry x y 
-    | sign2neq b a h₂ h₁ = eqReflexivity y
-  ...| False | False rewrite lte2ngt x y 
-    | sym $ ifFlip (y < x) b a = eqReflexivity (if (y < x) then b else a) 
+     | sign2neq b a h₂ h₁ = eqReflexivity y
+  ...| False | False 
+    rewrite lte2ngt x y 
+    | ifFlip (y < x) a b 
+    = eqReflexivity (if (y < x) then b else a) 
 
   iLawfulOrdInt .max2if a@(int64 x) b@(int64 y)
       with isNegativeInt a in h₁ | isNegativeInt b in h₂ 
-  ...| False | False rewrite gte2nlt x y | sym $ ifFlip (x < y) b a 
+  ...| False | False 
+    rewrite gte2nlt x y 
+    | ifFlip (x < y) a b
     = eqReflexivity (if (x < y) then b else a)
   ...| False | True  = eqReflexivity x
   ...| True  | False rewrite sign2neq a b h₁ h₂ 
     = eqReflexivity y
-  ...| True  | True  rewrite gte2nlt x y | sym $ ifFlip (x < y) b a 
+  ...| True  | True  
+    rewrite gte2nlt x y 
+    | ifFlip (x < y) a b
     = eqReflexivity (if (x < y) then b else a)

lib/Haskell/Law/Ord/Integer.agda

@@ -80,22 +80,22 @@ instance
 
   iLawfulOrdInteger .min2if (pos n)    (pos m) 
     rewrite lte2ngt n m
-    | sym $ ifFlip (m < n) (pos m) (pos n)  
+    | ifFlip (m < n) (pos n) (pos m)  
     = eqReflexivity (min (pos n) (pos m))
   iLawfulOrdInteger .min2if (pos n)    (negsuc m) = eqReflexivity m
   iLawfulOrdInteger .min2if (negsuc n) (pos m)    = eqReflexivity n
   iLawfulOrdInteger .min2if (negsuc n) (negsuc m) 
     rewrite gte2nlt n m  
-    | sym $ ifFlip (n < m) (negsuc m) (negsuc n) 
+    | ifFlip (n < m) (negsuc n) (negsuc m) 
     = eqReflexivity (min (negsuc n) (negsuc m)) 
 
   iLawfulOrdInteger .max2if (pos n)    (pos m) 
     rewrite gte2nlt n m 
-    | sym (ifFlip (n < m) (pos m) (pos n))  
+    | ifFlip (n < m) (pos n) (pos m)
     = eqReflexivity (max (pos n) (pos m)) 
   iLawfulOrdInteger .max2if (pos n)    (negsuc m) = eqReflexivity n  
   iLawfulOrdInteger .max2if (negsuc n) (pos m)    = eqReflexivity m 
   iLawfulOrdInteger .max2if (negsuc n) (negsuc m) 
     rewrite lte2ngt n m
-    | sym $ ifFlip (m < n) (negsuc m) (negsuc n) 
+    | ifFlip (m < n) (negsuc n) (negsuc m) 
     = eqReflexivity (max (negsuc n) (negsuc m))