FinMatrix.CoqExt.RExt.RExtBase

Require Export Basic Hierarchy.
Require Export Reals Lia Lra.
Open Scope R_scope.

#[export] Hint Unfold
  Rminus
  Rdiv
  
  : R.

#[global] Opaque
  PI exp sqrt Rpower ln
  sin cos tan asin atan acos
  up
.

#[export] Hint Resolve
  Rlt_0_1
  PI_RGT_0
  Rabs_pos
  Rgt_not_eq
  Rlt_not_eq
  : R.

Ltac ra :=
  intros;
  
  try match goal with | |- _ <-> _ => split; intros end;
  
  auto with R;
  try (unfold Rsqr in *; lra);
  try (unfold Rsqr in *; nra);
  try (unfold Rsqr in *; field; auto with R);
  
  autorewrite with R in *; auto with R;
  
  
  
  try (unfold Rsqr in *; lra);
  try (unfold Rsqr in *; nra);
  try (unfold Rsqr in *; field; auto with R)
.

Lemma R0_eq_0 : R0 = 0.
Proof. auto. Qed.
#[export] Hint Rewrite R0_eq_0 : R.

Lemma R1_eq_1 : R1 = 1.
Proof. auto. Qed.
#[export] Hint Rewrite R1_eq_1 : R.

Lemma zero_neq_1 : 0 <> 1.
Proof. lra. Qed.
#[export] Hint Resolve R1_eq_1 : R.

Lemma Rmult_ab_eq_a_imply : forall a b, a * b = a -> a = 0 \/ (a <> 0 /\ b = 1).
Proof. ra. Qed.

Lemma Rmult_ab_eq_b_imply : forall a b, a * b = b -> b = 0 \/ (b <> 0 /\ a = 1).
Proof. ra. Qed.

Section test.
  Variable a b c d e f g : R.
End test.