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