proposition: Theorem sub_gt : ∀ n m, m < n → n - m ≠ 0.
proof: Proof. intros n m Hmn. destruct n as [n| ]; simpl. destruct m as [m| ]; simpl. apply fin_lt_mono in Hmn. apply Nat.sub_gt in Hmn. intros H; apply Hmn. injection H; clear H; intros H; rewrite H; reflexivity. inversion Hmn. destruct m as [m| ]; simpl. intros H; discriminate H. inversion Hmn. Qed.
imports: Utf8 Compare_dec NPeano Misc