FinMatrix.CoqExt.RExt.RExtInv

Require Export RExtBase.

#[export] Hint Rewrite
  
  Rinv_1
  Rdiv_plus_distr
  Rsqr_div'
  Rdiv_mult_l_l
  Rdiv_mult_r_r
  : R.

Hint Rewrite
     <- Rdiv_def
  : R.

#[export] Hint Resolve
  
  Rinv_neq_0_compat
  Rinv_0_lt_compat
  Rinv_lt_0_compat
  
  Rdiv_lt_0_compat
  : R.

Lemma Rinv_R1 : / R1 = 1.
Proof. ra. Qed.
#[export] Hint Rewrite Rinv_R1 : R.

Lemma Rdiv_1 : forall a, a / 1 = a.
Proof. ra. Qed.
#[export] Hint Rewrite Rdiv_1 : R.

Lemma Rdiv_0_eq0 : forall a : R, a <> 0 -> 0 / a = 0.
Proof. ra. Qed.
#[export] Hint Rewrite Rdiv_0_eq0 : R.

Lemma Rinv_ab_simpl_a : forall r1 r2 r3,
    r1 <> 0 -> r3 <> 0 -> (r1 * r2) * / (r1 * r3) = r2 * / r3.
Proof. ra. Qed.
#[export] Hint Rewrite Rinv_ab_simpl_a : R.

Lemma Rinv_ab_simpl_b : forall r1 r2 r3,
    r2 <> 0 -> r3 <> 0 -> (r1 * r2) * / (r3 * r2) = r1 * / r3.
Proof. ra. Qed.
#[export] Hint Rewrite Rinv_ab_simpl_b : R.

Lemma Rdiv_1_neq_0_compat : forall r : R, r <> 0 -> 1 / r <> 0.
Proof. ra. pose proof (Rinv_neq_0_compat r H). ra. Qed.
#[export] Hint Resolve Rdiv_1_neq_0_compat : R.