proposition: Theorem lt_add_lt_sub_r : ∀ n m p, n + p < m ↔ n < m - p.
proof: Proof. intros n m p. split; intros H. destruct m as [m| ]; simpl. destruct p as [p| ]; simpl. destruct n as [n| ]; simpl. apply fin_lt_mono in H. apply fin_lt_mono. apply Nat.lt_add_lt_sub_r; assumption. exfalso; apply nle_gt in H; apply H; constructor. exfalso; apply nle_gt in H; apply H; rewrite add_comm; constructor. destruct p as [p| ]; simpl. destruct n as [n| ]; [ constructor | simpl ]. exfalso; apply nle_gt in H; apply H; constructor. exfalso; apply nle_gt in H; apply H; rewrite add_comm; constructor. destruct m as [m| ]; simpl. destruct p as [p| ]; simpl. destruct n as [n| ]; simpl. apply fin_lt_mono in H. apply fin_lt_mono. apply Nat.lt_add_lt_sub_r; assumption. exfalso; apply nle_gt in H; apply H; constructor. exfalso; apply nle_gt in H; apply H, le_0_l. destruct p as [p| ]; simpl. destruct n as [n| ]; [ constructor | simpl ]. exfalso; apply nle_gt in H; apply H; constructor. exfalso; apply nle_gt in H; apply H, le_0_l. Qed.
imports: Utf8 Compare_dec NPeano Misc