(**************************************************************************)
(*       ___                                                              *)
(*      ||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 "CoRN.ma".

(* $Id: COrdLemmas.v,v 1.2 2004/04/23 10:00:57 lcf Exp $ *)

include "algebra/COrdCauchy.ma".

(* UNEXPORTED
Section Lemmas
*)

(*#* *Lemmas for Integration

Here we include several lemmas valid in any ordered field [F] which 
are useful for integration.

** Merging orders

We first prove that any two strictly ordered sets of points which have
an empty intersection can be ordered as one (this will be the core of
the proof that any two partitions with no common point have a common
refinement).
*)

(* UNEXPORTED
cic:/CoRN/ftc/COrdLemmas/Lemmas/F.var
*)

inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_lt.con" as lemma.

inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun.con" as definition.

inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_1.con" as lemma.

inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_2a.con" as lemma.

inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_2.con" as lemma.

inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_3a.con" as lemma.

inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_3b.con" as lemma.

inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4a.con" as lemma.

inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4b.con" as lemma.

inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4c.con" as lemma.

inline procedural "cic:/CoRN/ftc/COrdLemmas/om_fun_4d.con" as lemma.

(* begin hide *)

(* UNEXPORTED
cic:/CoRN/ftc/COrdLemmas/Lemmas/f.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/COrdLemmas/Lemmas/f0.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/COrdLemmas/Lemmas/f_mon.var
*)

(* UNEXPORTED
cic:/CoRN/ftc/COrdLemmas/Lemmas/h.var
*)

(* end hide *)

(*#* ** Summations
Also, some technical stuff on sums.  The first lemma relates two
different kinds of sums; the other two ones are variations, where the
structure of the arguments is analyzed in more detail.
*)

(* begin show *)

inline procedural "cic:/CoRN/ftc/COrdLemmas/Sumx_Sum_Sum
 (* end show *)
 (* begin hide *).con" as lemma.

(* end hide *)

(* begin show *)

inline procedural "cic:/CoRN/ftc/COrdLemmas/str_Sumx_Sum_Sum
 (* end show *)
 (* begin hide *).con" as lemma.

(* UNEXPORTED
End Lemmas
*)

(* UNEXPORTED
Section More_Lemmas
*)

inline procedural "cic:/CoRN/ftc/COrdLemmas/More_Lemmas/f'.con" "More_Lemmas__" as definition.

(* end hide *)

(* UNEXPORTED
cic:/CoRN/ftc/COrdLemmas/More_Lemmas/F.var
*)

(* begin show *)

inline procedural "cic:/CoRN/ftc/COrdLemmas/str_Sumx_Sum_Sum'
 (* end show *)
 (* begin hide *).con" as lemma.

(* end hide *)

(* UNEXPORTED
End More_Lemmas
*)