proposition: Theorem sub_cancel_l n m p : n - m == n - p <-> m == p.
proof: Proof. rewrite <- (add_cancel_l (n - m) (n - p) (- n)). rewrite 2 add_sub_assoc. rewrite add_opp_diag_l; rewrite 2 sub_0_l. apply opp_inj_wd. Qed.
imports: ZBase