Proofs of preserving the last were added for + and *.

Author: buzden

libs/contrib/Data/Fin/Extra.idr

@@ -172,6 +172,16 @@ finToNat_mult_linearity (FS x) y {a=S i} = rewrite finToNat_plus_linearity y (x
                                            rewrite finToNat_mult_linearity x y in
                                            Refl
 
+export
+plus_preserves_last : (a, b : Nat) -> Fin.last {n=a} + Fin.last {n=b} = Fin.last
+plus_preserves_last Z     b = rewrite weakenNZero_preserves $ Fin.last {n=b} in Refl
+plus_preserves_last (S k) b = rewrite plus_preserves_last k b in Refl
+
+export
+mult_preserves_last : (a, b : Nat) -> Fin.last {n=a} * Fin.last {n=b} = Fin.last
+mult_preserves_last Z     b = Refl
+mult_preserves_last (S k) b = rewrite mult_preserves_last k b in plus_preserves_last _ _
+
 export
 plusSuccRightSucc : {a, b : Nat} -> (left : Fin $ S a) -> (right : Fin $ S b) -> FS (left + right) = rewrite plusSuccRightSucc a b in left + FS right
 plusSuccRightSucc FZ     right         = rewrite plusCommutative a b in Refl