If you define "≈" as part of asymptotic notation, like "A ≈ B as t → x" meaning "A−B ∈ o(1) as t → x", then you can indeed prove nice properties such as: If A ≈ B ≈ C as t → x, then A ≈ C as t → x. If A ≥ B ≈ C as t → x, then ( A > C or A ≈ C ) as t → x. If A ≈ B ≥ C as t → x, then ( A > C or A ...

True proof by contradiction is captured by the deductive rule ( ( ¬A ⇒ ⊥ ) ⊢ A ), which allows you to deduce A if you can deduce that ¬A implies a contradiction. Besides your chosen axioms, this rule is essentially the only non-constructive assumption you need in your foundational system for math...