Lemma natminusminus (n i j : nat) : n - i - j = n - (i + j). Proof. revert i j; induction n as [|n N]. - intros. apply idpath. - intros i; induction i as [|i _]. + intros. apply idpath. + apply N. Defined.