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