Z + n = n, (S n) + m = S (n + m)

PlusLike.idr

%default total

record PlusLike : (Nat -> Nat -> Nat) -> Type where
  PL : {plus : Nat -> Nat -> Nat} ->
       (plusIdentity : (n : Nat) -> plus Z n = n) ->
       (plusSucc : (n, m : Nat) -> plus (S n) m = S (plus n m)) ->
       PlusLike plus

isPlus : (f : Nat -> Nat -> Nat) -> PlusLike f -> (n, m : Nat) -> f n m = plus n m
isPlus f (PL plusIdentity _) Z m = plusIdentity m
isPlus f (PL plusIdentity plusSucc) (S k) m =
  let inductiveHypothesis = isPlus f (PL plusIdentity plusSucc) k m
  in ?isPlusStepCase

---------- Proofs ----------

isPlusStepCase = proof
  intros
  rewrite sym (plusSucc k m)
  rewrite inductiveHypothesis
  trivial