proposition: Theorem sub_add_distr : ∀ n m p, n - (m + p) = n - m - p.
proof: Proof. intros n m p. destruct m as [m| ]; [ simpl | destruct p; reflexivity ]. destruct p as [p| ]; [ simpl | reflexivity ]. destruct n as [n| ]; [ simpl | reflexivity ]. rewrite Nat.sub_add_distr; reflexivity. Qed.
imports: Utf8 Compare_dec NPeano Misc