proposition: Theorem sub_gt : forall n m, n > m -> n - m ~= 0.
proof: Proof. intros n m H; elim H using lt_ind_rel; clear n m H. - solve_proper. - intro; rewrite sub_0_r; apply neq_succ_0. - intros; now rewrite sub_succ. Qed.
imports: NMulOrder