proposition: Theorem sub_sub_distr : ∀ n m p, m ≠ ∞ → p ≤ m → n - (m - p) = n + p - m.
proof: Proof. intros n m p Hm Hpm. destruct m as [m| ]; [ idtac | exfalso; apply Hm; reflexivity ]. destruct p as [p| ]. destruct n as [n| ]; [ simpl | reflexivity ]. apply fin_le_mono in Hpm. rewrite Nat_sub_sub_distr; [ reflexivity | assumption ]. exfalso; apply nlt_ge in Hpm; apply Hpm; constructor. Qed.
imports: Utf8 Compare_dec NPeano Misc