(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* This file was automatically generated: do not edit *********************) include "Coq.ma". (*#***********************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* false) Rinv RTheory Rinv_l with minus := Rminus div := Rdiv. *) (*#*************************************************************************) (*#* Relation between orders and equality *) (*#*************************************************************************) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rlt_irrefl.con" as lemma. (* UNEXPORTED Hint Resolve Rlt_irrefl: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rle_refl.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rlt_not_eq.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rgt_not_eq.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rlt_dichotomy_converse.con" as lemma. (* UNEXPORTED Hint Resolve Rlt_dichotomy_converse: real. *) (*#* Reasoning by case on equalities and order *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Req_dec.con" as lemma. (* UNEXPORTED Hint Resolve Req_dec: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rtotal_order.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rdichotomy.con" as lemma. (*#********************************************************************************) (*#* Order Lemma : relating [<], [>], [<=] and [>=] *) (*#********************************************************************************) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rlt_le.con" as lemma. (* UNEXPORTED Hint Resolve Rlt_le: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rle_ge.con" as lemma. (* UNEXPORTED Hint Immediate Rle_ge: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rge_le.con" as lemma. (* UNEXPORTED Hint Resolve Rge_le: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rnot_le_lt.con" as lemma. (* UNEXPORTED Hint Immediate Rnot_le_lt: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rnot_ge_lt.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rlt_not_le.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rgt_not_le.con" as lemma. (* UNEXPORTED Hint Immediate Rlt_not_le: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rle_not_lt.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rlt_not_ge.con" as lemma. (* UNEXPORTED Hint Immediate Rlt_not_ge: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Req_le.con" as lemma. (* UNEXPORTED Hint Immediate Req_le: real. *) inline procedural "cic:/Coq/Reals/RIneq/Req_ge.con" as lemma. (* UNEXPORTED Hint Immediate Req_ge: real. *) inline procedural "cic:/Coq/Reals/RIneq/Req_le_sym.con" as lemma. (* UNEXPORTED Hint Immediate Req_le_sym: real. *) inline procedural "cic:/Coq/Reals/RIneq/Req_ge_sym.con" as lemma. (* UNEXPORTED Hint Immediate Req_ge_sym: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rle_antisym.con" as lemma. (* UNEXPORTED Hint Resolve Rle_antisym: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rle_le_eq.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rlt_eq_compat.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rle_trans.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rle_lt_trans.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rlt_le_trans.con" as lemma. (*#* Decidability of the order *) inline procedural "cic:/Coq/Reals/RIneq/Rlt_dec.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rle_dec.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rgt_dec.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rge_dec.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rlt_le_dec.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rle_or_lt.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rle_lt_or_eq_dec.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/inser_trans_R.con" as lemma. (*#***************************************************************) (*#* Field Lemmas *) (* This part contains lemma involving the Fields operations *) (*#***************************************************************) (*#********************************************************) (*#* Addition *) (*#********************************************************) inline procedural "cic:/Coq/Reals/RIneq/Rplus_ne.con" as lemma. (* UNEXPORTED Hint Resolve Rplus_ne: real v62. *) inline procedural "cic:/Coq/Reals/RIneq/Rplus_0_r.con" as lemma. (* UNEXPORTED Hint Resolve Rplus_0_r: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_opp_l.con" as lemma. (* UNEXPORTED Hint Resolve Rplus_opp_l: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_opp_r_uniq.con" as lemma. (*i New i*) (* UNEXPORTED Hint Resolve (f_equal (A:=R)): real. *) inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_compat_l.con" as lemma. (*i Old i*) (* UNEXPORTED Hint Resolve Rplus_eq_compat_l: v62. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_reg_l.con" as lemma. (* UNEXPORTED Hint Resolve Rplus_eq_reg_l: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_0_r_uniq.con" as lemma. (*#**********************************************************) (*#* Multiplication *) (*#**********************************************************) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rinv_r.con" as lemma. (* UNEXPORTED Hint Resolve Rinv_r: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rinv_l_sym.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_sym.con" as lemma. (* UNEXPORTED Hint Resolve Rinv_l_sym Rinv_r_sym: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_0_r.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_0_r: real v62. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_0_l.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_0_l: real v62. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_ne.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_ne: real v62. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_1_r.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_1_r: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_compat_l.con" as lemma. (*i OLD i*) (* UNEXPORTED Hint Resolve Rmult_eq_compat_l: v62. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_reg_l.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_integral.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_0_compat.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_eq_0_compat: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_0_compat_r.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_eq_0_compat_l.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_neq_0_reg.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_integral_contrapositive.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_integral_contrapositive: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_plus_distr_r.con" as lemma. (*#* Square function *) (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rsqr.con" as definition. (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rsqr_0.con" as lemma. (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rsqr_0_uniq.con" as lemma. (*#********************************************************) (*#* Opposite *) (*#********************************************************) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_eq_compat.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_eq_compat: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_0.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_0: real v62. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_eq_0_compat.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_eq_0_compat: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_involutive.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_involutive: real. *) (*#********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_neq_0_compat.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_neq_0_compat: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_plus_distr.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_plus_distr: real. *) (*#* Opposite and multiplication *) inline procedural "cic:/Coq/Reals/RIneq/Ropp_mult_distr_l_reverse.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_mult_distr_l_reverse: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_opp_opp.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_opp_opp: real. *) inline procedural "cic:/Coq/Reals/RIneq/Ropp_mult_distr_r_reverse.con" as lemma. (*#* Substraction *) inline procedural "cic:/Coq/Reals/RIneq/Rminus_0_r.con" as lemma. (* UNEXPORTED Hint Resolve Rminus_0_r: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rminus_0_l.con" as lemma. (* UNEXPORTED Hint Resolve Rminus_0_l: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_minus_distr.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_minus_distr: real. *) inline procedural "cic:/Coq/Reals/RIneq/Ropp_minus_distr'.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_minus_distr': real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rminus_diag_eq.con" as lemma. (* UNEXPORTED Hint Resolve Rminus_diag_eq: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rminus_diag_uniq.con" as lemma. (* UNEXPORTED Hint Immediate Rminus_diag_uniq: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rminus_diag_uniq_sym.con" as lemma. (* UNEXPORTED Hint Immediate Rminus_diag_uniq_sym: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rplus_minus.con" as lemma. (* UNEXPORTED Hint Resolve Rplus_minus: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rminus_eq_contra.con" as lemma. (* UNEXPORTED Hint Resolve Rminus_eq_contra: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rminus_not_eq.con" as lemma. (* UNEXPORTED Hint Resolve Rminus_not_eq: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rminus_not_eq_right.con" as lemma. (* UNEXPORTED Hint Resolve Rminus_not_eq_right: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_minus_distr_l.con" as lemma. (*#* Inverse *) inline procedural "cic:/Coq/Reals/RIneq/Rinv_1.con" as lemma. (* UNEXPORTED Hint Resolve Rinv_1: real. *) (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rinv_neq_0_compat.con" as lemma. (* UNEXPORTED Hint Resolve Rinv_neq_0_compat: real. *) (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rinv_involutive.con" as lemma. (* UNEXPORTED Hint Resolve Rinv_involutive: real. *) (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rinv_mult_distr.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_inv_permute.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_simpl_r.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_simpl_l.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rinv_r_simpl_m.con" as lemma. (* UNEXPORTED Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: real. *) (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rinv_mult_simpl.con" as lemma. (*#* Order and addition *) inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_compat_r.con" as lemma. (* UNEXPORTED Hint Resolve Rplus_lt_compat_r: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_reg_r.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_compat_l.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_compat_r.con" as lemma. (* UNEXPORTED Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_reg_l.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/sum_inequa_Rle_lt.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_compat.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_compat.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_le_compat.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_lt_compat.con" as lemma. (* UNEXPORTED Hint Immediate Rplus_lt_compat Rplus_le_compat Rplus_lt_le_compat Rplus_le_lt_compat: real. *) (*#* Order and Opposite *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_gt_lt_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_gt_lt_contravar. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_gt_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_lt_gt_contravar: real. *) inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_cancel.con" as lemma. (* UNEXPORTED Hint Immediate Ropp_lt_cancel: real. *) inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_lt_contravar: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_le_ge_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_le_ge_contravar: real. *) inline procedural "cic:/Coq/Reals/RIneq/Ropp_le_cancel.con" as lemma. (* UNEXPORTED Hint Immediate Ropp_le_cancel: real. *) inline procedural "cic:/Coq/Reals/RIneq/Ropp_le_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_le_contravar: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_ge_le_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_ge_le_contravar: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_lt_gt_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_0_lt_gt_contravar: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_gt_lt_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_0_gt_lt_contravar: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_lt_gt_0_contravar.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_gt_lt_0_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_lt_gt_0_contravar Ropp_gt_lt_0_contravar: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_le_ge_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_0_le_ge_contravar: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_0_ge_le_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Ropp_0_ge_le_contravar: real. *) (*#* Order and multiplication *) inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_compat_r.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_lt_compat_r. *) inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_reg_l.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_gt_compat_neg_l.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat_l.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_le_compat_l: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat_r.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_le_compat_r: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_reg_l.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat_neg_l.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_le_compat_neg_l: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_ge_compat_neg_l.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_le_ge_compat_neg_l: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_compat.con" as lemma. (* UNEXPORTED Hint Resolve Rmult_le_compat: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rmult_gt_0_lt_compat.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_ge_0_gt_0_lt_compat.con" as lemma. (*#* Order and Substractions *) inline procedural "cic:/Coq/Reals/RIneq/Rlt_minus.con" as lemma. (* UNEXPORTED Hint Resolve Rlt_minus: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rle_minus.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rminus_lt.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rminus_le.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/tech_Rplus.con" as lemma. (* UNEXPORTED Hint Immediate tech_Rplus: real. *) (*#* Order and the square function *) inline procedural "cic:/Coq/Reals/RIneq/Rle_0_sqr.con" as lemma. (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rlt_0_sqr.con" as lemma. (* UNEXPORTED Hint Resolve Rle_0_sqr Rlt_0_sqr: real. *) (*#* Zero is less than one *) inline procedural "cic:/Coq/Reals/RIneq/Rlt_0_1.con" as lemma. (* UNEXPORTED Hint Resolve Rlt_0_1: real. *) inline procedural "cic:/Coq/Reals/RIneq/Rle_0_1.con" as lemma. (*#* Order and inverse *) inline procedural "cic:/Coq/Reals/RIneq/Rinv_0_lt_compat.con" as lemma. (* UNEXPORTED Hint Resolve Rinv_0_lt_compat: real. *) (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rinv_lt_0_compat.con" as lemma. (* UNEXPORTED Hint Resolve Rinv_lt_0_compat: real. *) (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rinv_lt_contravar.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rinv_1_lt_contravar.con" as lemma. (* UNEXPORTED Hint Resolve Rinv_1_lt_contravar: real. *) (*#********************************************************) (*#* Greater *) (*#********************************************************) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rge_antisym.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rnot_lt_ge.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rnot_lt_le.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rnot_gt_le.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rgt_ge.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rge_gt_trans.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rgt_ge_trans.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rgt_trans.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rge_trans.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rle_lt_0_plus_1.con" as lemma. (* UNEXPORTED Hint Resolve Rle_lt_0_plus_1: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rlt_plus_1.con" as lemma. (* UNEXPORTED Hint Resolve Rlt_plus_1: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/tech_Rgt_minus.con" as lemma. (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_gt_compat_l.con" as lemma. (* UNEXPORTED Hint Resolve Rplus_gt_compat_l: real. *) (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_gt_reg_l.con" as lemma. (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_ge_compat_l.con" as lemma. (* UNEXPORTED Hint Resolve Rplus_ge_compat_l: real. *) (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_ge_reg_l.con" as lemma. (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_ge_compat_r.con" as lemma. (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rgt_minus.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/minus_Rgt.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Rge_minus.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/minus_Rge.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_gt_0_compat.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_lt_0_compat.con" as lemma. (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_0_l.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rplus_eq_R0.con" as lemma. (*#**********) inline procedural "cic:/Coq/Reals/RIneq/Rplus_sqr_eq_0_l.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rplus_sqr_eq_0.con" as lemma. (*#*********************************************************) (*#* Injection from [N] to [R] *) (*#*********************************************************) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/S_INR.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/S_O_plus_INR.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/plus_INR.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/minus_INR.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/mult_INR.con" as lemma. (* UNEXPORTED Hint Resolve plus_INR minus_INR mult_INR: real. *) (*#********) inline procedural "cic:/Coq/Reals/RIneq/lt_INR_0.con" as lemma. (* UNEXPORTED Hint Resolve lt_INR_0: real. *) inline procedural "cic:/Coq/Reals/RIneq/lt_INR.con" as lemma. (* UNEXPORTED Hint Resolve lt_INR: real. *) inline procedural "cic:/Coq/Reals/RIneq/INR_lt_1.con" as lemma. (* UNEXPORTED Hint Resolve INR_lt_1: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/INR_pos.con" as lemma. (* UNEXPORTED Hint Resolve INR_pos: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/pos_INR.con" as lemma. (* UNEXPORTED Hint Resolve pos_INR: real. *) inline procedural "cic:/Coq/Reals/RIneq/INR_lt.con" as lemma. (* UNEXPORTED Hint Resolve INR_lt: real. *) (*#********) inline procedural "cic:/Coq/Reals/RIneq/le_INR.con" as lemma. (* UNEXPORTED Hint Resolve le_INR: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/not_INR_O.con" as lemma. (* UNEXPORTED Hint Immediate not_INR_O: real. *) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/not_O_INR.con" as lemma. (* UNEXPORTED Hint Resolve not_O_INR: real. *) inline procedural "cic:/Coq/Reals/RIneq/not_nm_INR.con" as lemma. (* UNEXPORTED Hint Resolve not_nm_INR: real. *) inline procedural "cic:/Coq/Reals/RIneq/INR_eq.con" as lemma. (* UNEXPORTED Hint Resolve INR_eq: real. *) inline procedural "cic:/Coq/Reals/RIneq/INR_le.con" as lemma. (* UNEXPORTED Hint Resolve INR_le: real. *) inline procedural "cic:/Coq/Reals/RIneq/not_1_INR.con" as lemma. (* UNEXPORTED Hint Resolve not_1_INR: real. *) (*#*********************************************************) (*#* Injection from [Z] to [R] *) (*#*********************************************************) (*#*********) inline procedural "cic:/Coq/Reals/RIneq/IZN.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/INR_IZR_INZ.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/plus_IZR_NEG_POS.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/plus_IZR.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/mult_IZR.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Ropp_Ropp_IZR.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/Z_R_minus.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/lt_O_IZR.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/lt_IZR.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/eq_IZR_R0.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/eq_IZR.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/not_O_IZR.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/le_O_IZR.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/le_IZR.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/le_IZR_R1.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/IZR_ge.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/IZR_le.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/IZR_lt.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/one_IZR_lt1.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/one_IZR_r_R1.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/single_z_r_R1.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/tech_single_z_r_R1.con" as lemma. (*#****************************************************************) (*#* Definitions of new types *) (*#****************************************************************) inline procedural "cic:/Coq/Reals/RIneq/nonnegreal.ind". inline procedural "cic:/Coq/Reals/RIneq/posreal.ind". inline procedural "cic:/Coq/Reals/RIneq/nonposreal.ind". inline procedural "cic:/Coq/Reals/RIneq/negreal.ind". inline procedural "cic:/Coq/Reals/RIneq/nonzeroreal.ind". (*#*********) inline procedural "cic:/Coq/Reals/RIneq/prod_neq_R0.con" as lemma. (*#********) inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_pos.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/double.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/double_var.con" as lemma. (*#*********************************************************) (*#* Other rules about < and <= *) (*#*********************************************************) inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_0_compat.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_lt_0_compat.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rplus_lt_le_0_compat.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rplus_le_le_0_compat.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/plus_le_is_le.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/plus_lt_is_lt.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/Rmult_le_0_lt_compat.con" as lemma. inline procedural "cic:/Coq/Reals/RIneq/le_epsilon.con" as lemma. (*#*********) inline procedural "cic:/Coq/Reals/RIneq/completeness_weak.con" as lemma.