
  0 | module Algebra.Solver.Ring.Util
  1 | 
  2 | import Algebra.Ring
  3 | import public Syntax.PreorderReasoning
  4 | 
  5 | %default total
  6 | 
  7 | export
  8 | 0 p213 : Ring a => {k,m,n : a} -> k + (m + n) === m + (k + n)
  9 | p213 = Calc $
 10 |   |~ k + (m + n)
 11 |   ~~ (k + m) + n   ... plusAssociative
 12 |   ~~ (m + k) + n   ... cong (+n) plusCommutative
 13 |   ~~ m + (k + n)   ..< plusAssociative
 14 | 
 15 | export
 16 | 0 p1324 :
 17 |      {auto _ : Ring a}
 18 |   -> {k,l,m,n : a}
 19 |   -> (k + l) + (m + n) === (k + m) + (l + n)
 20 | p1324 = Calc $
 21 |   |~ (k + l) + (m + n)
 22 |   ~~ ((k + l) + m) + n ... plusAssociative
 23 |   ~~ (k + (l + m)) + n ..< cong (+n) plusAssociative
 24 |   ~~ (k + (m + l)) + n ... cong (\x => (k + x) + n) plusCommutative
 25 |   ~~ ((k + m) + l) + n ... cong (+n) plusAssociative
 26 |   ~~ (k + m) + (l + n) ..< plusAssociative
 27 | 
 28 | export
 29 | 0 m1324 :
 30 |      {auto _ : Ring a}
 31 |   -> {k,l,m,n : a}
 32 |   -> (k * l) * (m * n) === (k * m) * (l * n)
 33 | m1324 = Calc $
 34 |   |~ (k * l) * (m * n)
 35 |   ~~ ((k * l) * m) * n ... multAssociative
 36 |   ~~ (k * (l * m)) * n ..< cong (*n) multAssociative
 37 |   ~~ (k * (m * l)) * n ... cong (\x => (k * x) * n) multCommutative
 38 |   ~~ ((k * m) * l) * n ... cong (*n) multAssociative
 39 |   ~~ (k * m) * (l * n) ..< multAssociative
 40 |