FinMatrix.CoqExt.RExt.RExtPlus

Require Export RExtBase.

#[export] Hint Rewrite
  Rplus_0_l
  Rplus_0_r
  : R.

Lemma Rplus_eq0_if_both0 : forall a b : R, a = 0 -> b = 0 -> a + b = 0.
Proof. intros. subst. lra. Qed.
#[export] Hint Resolve Rplus_eq0_if_both0 : R.

Lemma Rplus_eq_0_r : forall a b : R, 0 <= a -> 0 <= b -> a + b = 0 -> b = 0.
Proof. intros. lra. Qed.