proposition: Theorem add_sub_eq_nz : forall n m p, p ~= 0 -> n - m == p -> m + p == n.
proof: Proof. intros n m p H; double_induct n m. - intros m H1; rewrite sub_0_l in H1. symmetry in H1; false_hyp H1 H. - intro n; rewrite sub_0_r; now rewrite add_0_l. - intros n m IH H1. rewrite sub_succ in H1. apply IH in H1. rewrite add_succ_l; now rewrite H1. Qed.
imports: NMulOrder