proposition: Theorem sub_0_le : forall n m, n - m == 0 <-> n <= m.
proof: Proof. intros n m; double_induct n m. - intro m; split; intro; [apply le_0_l | apply sub_0_l]. - intro m; rewrite sub_0_r; split; intro H; [false_hyp H neq_succ_0 | false_hyp H nle_succ_0]. - intros n m H. rewrite <- succ_le_mono. now rewrite sub_succ. Qed.
imports: NMulOrder