proposition: Lemma Rinv_1 : forall x, x * / 1 = x.
proof: Proof. intro. rewrite Rinv_1. apply Rmult_1_r. Qed.
imports: OrderedRing QMicromega RingMicromega Refl Sumbool Raxioms Rfunctions RIneq Rpow_def QArith Qfield Qreals DeclConstant