FinMatrix.CoqExt.RExt.RExtPlus


Require Export RExtBase.

Basic automation


Hint Rewrite
  Rplus_0_l
  Rplus_0_r
  : R.


Additional properties

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

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