initial from another archive

FiniteDim/gram_schmidt.v

+Require Export Coquelicot.Coquelicot.
+Require Export Reals.
+Require Export mathcomp.ssreflect.ssreflect.
+Require Export FunctionalExtensionality.
+Require Export hilbert.
+Require Export lax_milgram.
+Require Import Program ZArith.
+
+Context {E : Hilbert}.
+
+Program Fixpoint GS (B : nat -> E) (n : nat) { measure n } :=
+ match n with
+ | O => B O
+ | S k => minus (B (S k)) (sum_n (fun j => match (le_dec j k) with
+                                           |left _ => GS B j
+                                           |right _ => zero end) k)
+end.
+Next Obligation.
+Proof.
+omega.
+Qed.
+
+Program Fixpoint GS' (B : nat -> E) (n : nat) { measure n } :=
+ match n with
+ | O => B O
+ | S k => minus (B (S k)) (sum_n (fun j => GS' B j) k)
+end.
+Next Obligation.
+Proof.
+admit.
+Admitted.
+
+Lemma GS'_fix (B : nat -> E) : forall n : nat, GS' B n =
+ match n with
+ | O => B O
+ | S k => minus (B (S k)) (sum_n (fun j => GS' B j) k)
+end.
+Proof.
+intros n.
+unfold GS' at 1.
+unfold GS'_func.
+rewrite WfExtensionality.fix_sub_eq_ext.
+fold GS'.
+fold GS'.
+destruct n.
+auto.
+destruct n.
+auto. auto.
+Qed.

LM/CoqMakefile.conf

+# This configuration file was generated by running:
+# coq_makefile
+
+
+###############################################################################
+#                                                                             #
+# Project files.                                                              #
+#                                                                             #
+###############################################################################
+
+COQMF_VFILES = 
+COQMF_MLIFILES = 
+COQMF_MLFILES = 
+COQMF_ML4FILES = 
+COQMF_MLPACKFILES = 
+COQMF_MLLIBFILES = 
+COQMF_CMDLINE_VFILES = 
+
+###############################################################################
+#                                                                             #
+# Path directives (-I, -R, -Q).                                               #
+#                                                                             #
+###############################################################################
+
+COQMF_OCAMLLIBS = 
+COQMF_SRC_SUBDIRS = 
+COQMF_COQLIBS =   
+COQMF_COQLIBS_NOML =  
+COQMF_CMDLINE_COQLIBS =   
+
+###############################################################################
+#                                                                             #
+# Coq configuration.                                                          #
+#                                                                             #
+###############################################################################
+
+COQMF_LOCAL=0
+COQMF_COQLIB=/home/mayero/opam-coq.8.8.2/ocaml-base-compiler.4.02.3/lib/coq/
+COQMF_DOCDIR=/home/mayero/opam-coq.8.8.2/ocaml-base-compiler.4.02.3/doc/
+COQMF_OCAMLFIND=/home/mayero/opam-coq.8.8.2/ocaml-base-compiler.4.02.3/bin/ocamlfind
+COQMF_CAMLP5O=/home/mayero/opam-coq.8.8.2/ocaml-base-compiler.4.02.3/bin/camlp5o
+COQMF_CAMLP5BIN=/home/mayero/opam-coq.8.8.2/ocaml-base-compiler.4.02.3/bin/
+COQMF_CAMLP5LIB=/home/mayero/opam-coq.8.8.2/ocaml-base-compiler.4.02.3/lib/camlp5
+COQMF_CAMLP5OPTIONS=-loc loc
+COQMF_CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50-58-59   -safe-string
+COQMF_HASNATDYNLINK=true
+COQMF_COQ_SRC_SUBDIRS=config dev lib clib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml
+COQMF_WINDRIVE=
+
+###############################################################################
+#                                                                             #
+# Extra variables.                                                            #
+#                                                                             #
+###############################################################################
+
+COQMF_OTHERFLAGS = 
+COQMF_INSTALLCOQDOCROOT = orphan_

LM/Makefile

+#############################################################################
+##  v      #                   The Coq Proof Assistant                     ##
+## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
+##   \VV/  #                                                               ##
+##    //   #  Makefile automagically generated by coq_makefile V8.6.1      ##
+#############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile -R . LM check_sub_structure.v compatible.v continuous_linear_map.v fixed_point.v hierarchyD.v hilbert.v lax_milgram.v linear_map.v logic_tricks.v R_compl.v lax_milgram_cea.v 
+#
+
+.DEFAULT_GOAL := all
+
+# This Makefile may take arguments passed as environment variables:
+# COQBIN to specify the directory where Coq binaries resides;
+# TIMECMD set a command to log .v compilation time;
+# TIMED if non empty, use the default time command as TIMECMD;
+# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
+# DSTROOT to specify a prefix to install path.
+# VERBOSE to disable the short display of compilation rules.
+
+VERBOSE?=
+SHOW := $(if $(VERBOSE),@true "",@echo "")
+HIDE := $(if $(VERBOSE),,@)
+
+# Here is a hack to make $(eval $(shell works:
+define donewline
+
+
+endef
+includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
+$(call includecmdwithout@,$(COQBIN)coqtop -config)
+
+TIMED?=
+TIMECMD?=
+STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
+TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
+
+vo_to_obj = $(addsuffix .o,\
+  $(filter-out Warning: Error:,\
+  $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))
+
+##########################
+#                        #
+# Libraries definitions. #
+#                        #
+##########################
+
+COQLIBS?=\
+  -R "." LM
+COQCHKLIBS?=\
+  -R "." LM
+COQDOCLIBS?=\
+  -R "." LM
+
+##########################
+#                        #
+# Variables definitions. #
+#                        #
+##########################
+
+
+OPT?=
+COQDEP?="$(COQBIN)coqdep" -c
+COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
+COQCHKFLAGS?=-silent -o
+COQDOCFLAGS?=-interpolate -utf8
+COQC?=$(TIMER) "$(COQBIN)coqc"
+GALLINA?="$(COQBIN)gallina"
+COQDOC?="$(COQBIN)coqdoc"
+COQCHK?="$(COQBIN)coqchk"
+COQMKTOP?="$(COQBIN)coqmktop"
+
+##################
+#                #
+# Install Paths. #
+#                #
+##################
+
+ifdef USERINSTALL
+XDG_DATA_HOME?="$(HOME)/.local/share"
+COQLIBINSTALL=$(XDG_DATA_HOME)/coq
+COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
+else
+COQLIBINSTALL="${COQLIB}user-contrib"
+COQDOCINSTALL="${DOCDIR}user-contrib"
+COQTOPINSTALL="${COQLIB}toploop"
+endif
+
+######################
+#                    #
+# Files dispatching. #
+#                    #
+######################
+
+VFILES:=check_sub_structure.v\
+  compatible.v\
+  continuous_linear_map.v\
+  fixed_point.v\
+  hierarchyD.v\
+  hilbert.v\
+  lax_milgram.v\
+  linear_map.v\
+  logic_tricks.v\
+  R_compl.v\
+  lax_milgram_cea.v
+
+ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
+-include $(addsuffix .d,$(VFILES))
+else
+ifeq ($(MAKECMDGOALS),)
+-include $(addsuffix .d,$(VFILES))
+endif
+endif
+
+.SECONDARY: $(addsuffix .d,$(VFILES))
+
+VO=vo
+VOFILES:=$(VFILES:.v=.$(VO))
+GLOBFILES:=$(VFILES:.v=.glob)
+GFILES:=$(VFILES:.v=.g)
+HTMLFILES:=$(VFILES:.v=.html)
+GHTMLFILES:=$(VFILES:.v=.g.html)
+OBJFILES=$(call vo_to_obj,$(VOFILES))
+ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
+NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
+ifeq '$(HASNATDYNLINK)' 'true'
+HASNATDYNLINK_OR_EMPTY := yes
+else
+HASNATDYNLINK_OR_EMPTY :=
+endif
+
+#######################################
+#                                     #
+# Definition of the toplevel targets. #
+#                                     #
+#######################################
+
+all: $(VOFILES) 
+
+quick: $(VOFILES:.vo=.vio)
+
+vio2vo:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
+checkproofs:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
+gallina: $(GFILES)
+
+html: $(GLOBFILES) $(VFILES)
+	- mkdir -p html
+	$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
+
+gallinahtml: $(GLOBFILES) $(VFILES)
+	- mkdir -p html
+	$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
+
+all.ps: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all-gal.ps: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all.pdf: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+all-gal.pdf: $(VFILES)
+	$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
+
+validate: $(VOFILES)
+	$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))
+
+beautify: $(VFILES:=.beautified)
+	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
+	@echo 'Do not do "make clean" until you are sure that everything went well!'
+	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
+
+.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo
+
+####################
+#                  #
+# Special targets. #
+#                  #
+####################
+
+byte:
+	$(MAKE) all "OPT:=-byte"
+
+opt:
+	$(MAKE) all "OPT:=-opt"
+
+userinstall:
+	+$(MAKE) USERINSTALL=true install
+
+install:
+	cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \
+	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/LM/$$i`"; \
+	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/LM/$$i; \
+	done
+
+install-doc:
+	install -d "$(DSTROOT)"$(COQDOCINSTALL)/LM/html
+	for i in html/*; do \
+	 install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/LM/$$i;\
+	done
+
+uninstall_me.sh: Makefile
+	echo '#!/bin/sh' > $@
+	printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/LM && rm -f $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "LM" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
+	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/LM \\\n' >> "$@"
+	printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@"
+	printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find LM/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@"
+	chmod +x $@
+
+uninstall: uninstall_me.sh
+	sh $<
+
+.merlin:
+	@echo 'FLG -rectypes' > .merlin
+	@echo "B $(COQLIB)kernel" >> .merlin
+	@echo "B $(COQLIB)lib" >> .merlin
+	@echo "B $(COQLIB)library" >> .merlin
+	@echo "B $(COQLIB)parsing" >> .merlin
+	@echo "B $(COQLIB)pretyping" >> .merlin
+	@echo "B $(COQLIB)interp" >> .merlin
+	@echo "B $(COQLIB)printing" >> .merlin
+	@echo "B $(COQLIB)intf" >> .merlin
+	@echo "B $(COQLIB)proofs" >> .merlin
+	@echo "B $(COQLIB)tactics" >> .merlin
+	@echo "B $(COQLIB)tools" >> .merlin
+	@echo "B $(COQLIB)ltacprof" >> .merlin
+	@echo "B $(COQLIB)toplevel" >> .merlin
+	@echo "B $(COQLIB)stm" >> .merlin
+	@echo "B $(COQLIB)grammar" >> .merlin
+	@echo "B $(COQLIB)config" >> .merlin
+	@echo "B $(COQLIB)ltac" >> .merlin
+	@echo "B $(COQLIB)engine" >> .merlin
+
+clean::
+	rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES)
+	find . -name .coq-native -type d -empty -delete
+	rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
+	rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
+	- rm -rf html mlihtml uninstall_me.sh
+
+cleanall:: clean
+	rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
+
+archclean::
+	rm -f *.cmx *.o
+
+printenv:
+	@"$(COQBIN)coqtop" -config
+	@echo 'OCAMLFIND =	$(OCAMLFIND)'
+	@echo 'PP =	$(PP)'
+	@echo 'COQFLAGS =	$(COQFLAGS)'
+	@echo 'COQLIBINSTALL =	$(COQLIBINSTALL)'
+	@echo 'COQDOCINSTALL =	$(COQDOCINSTALL)'
+
+###################
+#                 #
+# Implicit rules. #
+#                 #
+###################
+
+$(VOFILES): %.vo: %.v
+	$(SHOW)COQC $<
+	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<
+
+$(GLOBFILES): %.glob: %.v
+	$(COQC) $(COQDEBUG) $(COQFLAGS) $<
+
+$(VFILES:.v=.vio): %.vio: %.v
+	$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<
+
+$(GFILES): %.g: %.v
+	$(GALLINA) $<
+
+$(VFILES:.v=.tex): %.tex: %.v
+	$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
+
+$(HTMLFILES): %.html: %.v %.glob
+	$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
+
+$(VFILES:.v=.g.tex): %.g.tex: %.v
+	$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
+
+$(GHTMLFILES): %.g.html: %.v %.glob
+	$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
+
+$(addsuffix .d,$(VFILES)): %.v.d: %.v
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+$(addsuffix .beautified,$(VFILES)): %.v.beautified:
+	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v
+
+# WARNING
+#
+# This Makefile has been automagically generated
+# Edit at your own risks !
+#
+# END OF WARNING
+

LM/R_compl.v

+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+Require Export Reals Coquelicot.Coquelicot.
+
+Open Scope R_scope.
+
+Section RC.
+
+(** If a degree-2 polynomial is always nonnegative, its dicriminant is nonpositive *)
+
+Lemma discr_neg: forall a b c,
+  (forall x, 0 <= a*x*x+b*x+c) ->
+     b*b-4*a*c <= 0.
+intros.
+case (Req_dec a 0); intros H'.
+cut (b=0).
+intros H1; rewrite H'; rewrite H1.
+right; ring.
+case (Req_dec b 0); trivial; intros.
+absurd (0 <= a*((-c-1)/b)*((-c-1)/b)+b*((-c-1)/b)+c).
+2: apply H.
+apply Rlt_not_le.
+rewrite H'; apply Rle_lt_trans with (-1).
+right; field; trivial.
+apply Ropp_lt_gt_0_contravar; apply Rlt_gt; auto with real.
+assert (0 <= c).
+apply Rle_trans with (a*0*0+b*0+c);[idtac|right; ring].
+apply H.
+assert (0 < a).
+cut (0 <= a).
+intros T; case T;auto with real.
+intros T'; absurd (a=0); auto.
+case (Req_dec b 0); intros.
+case (Rle_or_lt 0 a); trivial; intros.
+absurd (0 <= a* sqrt ((c+1)/(-a)) * sqrt ((c+1)/(-a)) +b*sqrt ((c+1)/(-a))+c).
+2: apply H.
+apply Rlt_not_le.
+rewrite H1; ring_simplify ( 0 * sqrt ((c + 1) / - a)).
+rewrite Rmult_assoc.
+rewrite sqrt_sqrt.
+apply Rle_lt_trans with (-1).
+right; field; auto with real.
+apply Ropp_lt_gt_0_contravar; apply Rlt_gt; auto with real.
+unfold Rdiv; apply Rmult_le_pos; auto with real.
+case H0; intros.
+apply Rmult_le_reg_l with (c*c/(b*b)).
+unfold Rdiv; apply Rmult_lt_0_compat.
+apply Rmult_lt_0_compat; trivial.
+apply Rinv_0_lt_compat.
+fold (Rsqr b); auto with real.
+ring_simplify.
+apply Rle_trans with (a*(-c/b)*(-c/b)+b*(-c/b)+c).
+apply H.
+right; field; trivial.
+apply Rmult_le_reg_l with (b*b).
+fold (Rsqr b); auto with real.
+ring_simplify.
+apply Rle_trans with (Rsqr b); auto with real.
+apply Rplus_le_reg_l with (-Rsqr b); ring_simplify.
+apply Rle_trans with (a*(-b)*(-b)+b*(-b)+c).
+apply H.
+rewrite <- H2; unfold Rsqr; right; ring.
+case (Rle_or_lt (b * b - 4 * a * c) 0); trivial.
+intros H2.
+absurd ( 0 <= a * (-b/(2*a)) * (-b/(2*a)) + b * (-b/(2*a)) + c).
+apply Rlt_not_le.
+replace (a * (- b / (2*a)) * (- b / (2*a)) + b * (- b / (2*a)) + c) with
+  (-b*b/(4*a)+c).
+apply Rmult_lt_reg_l with (4*a).
+repeat apply Rmult_lt_0_compat; auto with real.
+apply Rplus_lt_reg_r with (b*b-4*a*c).
+apply Rle_lt_trans with 0%R.
+right; field; auto.
+apply Rlt_le_trans with (1:=H2); right; ring.
+field; auto.
+apply H.
+Qed.
+
+Lemma contraction_lt_any: forall k d, 0 <= k < 1 -> 0 < d -> exists N, pow k N < d.
+Proof.
+intros k d Hk Hd.
+case (proj1 Hk); intros Hk'.
+(* 0 < k *)
+assert (ln k < 0).
+rewrite <- ln_1.
+apply ln_increasing; try apply Hk; assumption.
+exists (Z.abs_nat (up (ln d / ln k))).
+apply ln_lt_inv; try assumption.
+now apply pow_lt.
+rewrite <- Rpower_pow; trivial.
+unfold Rpower.
+rewrite ln_exp.
+apply Rmult_lt_reg_l with (- /ln k).
+apply Ropp_gt_lt_0_contravar.
+now apply Rinv_lt_0_compat.
+apply Rle_lt_trans with (-(INR (Z.abs_nat (up (ln d / ln k))))).
+right; field.
+now apply Rlt_not_eq.
+rewrite Ropp_mult_distr_l_reverse.
+apply Ropp_lt_contravar.
+generalize (archimed (ln d / ln k)); intros (Y1,_).
+rewrite Rmult_comm.
+apply Rlt_le_trans with (1:=Y1).
+generalize (up (ln d / ln k)); clear; intros x.
+rewrite INR_IZR_INZ, Zabs2Nat.id_abs.
+apply IZR_le.
+case (Zabs_spec x); intros (T1,T2); rewrite T2; auto with zarith.
+(* k = 0 *)
+exists 1%nat.
+rewrite <- Hk';simpl.
+now rewrite Rmult_0_l.
+Qed.
+
+Lemma contraction_lt_any': forall k d, 0 <= k < 1 -> 0 < d -> exists N, (0 < N)%nat /\ pow k N < d.
+Proof.
+intros k d H1 H2.
+destruct (contraction_lt_any k d H1 H2) as (N,HN).
+case_eq N.
+intros H3; exists 1%nat; split.
+now apply le_n.
+rewrite H3 in HN; simpl in HN.
+simpl; rewrite Rmult_1_r.
+now apply Rlt_trans with 1.
+intros m Hm.
+exists N; split; try assumption.
+rewrite Hm.
+now auto with arith.
+Qed.
+
+Lemma Rinv_le_cancel: forall x y : R, 0 < y -> / y <= / x -> x <= y.
+Proof.
+intros x y H1 H2.
+case (Req_dec x 0); intros Hx.
+rewrite Hx; now left.
+destruct H2.
+left; now apply Rinv_lt_cancel.
+right; rewrite <- Rinv_involutive.
+2: now apply Rgt_not_eq.
+rewrite H.
+now apply sym_eq, Rinv_involutive.
+Qed.
+
+Lemma Rlt_R1_pow: forall x n, 0 <= x < 1 -> (0 < n)%nat -> x ^ n < 1.
+Proof.
+intros x n (Hx1,Hx2) Hn.
+case (Req_dec x 0); intros H'.
+rewrite H', pow_i; try assumption.
+apply Rlt_0_1.
+apply Rinv_lt_cancel.
+apply Rlt_0_1.
+rewrite Rinv_1.
+rewrite Rinv_pow; try assumption.
+apply Rlt_pow_R1; try assumption.
+rewrite <- Rinv_1.
+apply Rinv_lt_contravar; try assumption.
+rewrite Rmult_1_r.
+destruct Hx1; trivial.
+contradict H; now apply not_eq_sym.
+Qed.
+
+Lemma Rle_pow_le: forall (x : R) (m n : nat), 0 < x <= 1 -> (m <= n)%nat -> x ^ n <= x ^ m.
+Proof.
+intros x m n (Hx1,Hx2) H.
+apply Rinv_le_cancel.
+now apply pow_lt.
+rewrite 2!Rinv_pow; try now apply Rgt_not_eq.
+apply Rle_pow; try assumption.
+rewrite <- Rinv_1.
+apply Rinv_le_contravar; try assumption.
+Qed.
+
+Lemma is_finite_betw: forall x y z,
+  Rbar_le (Finite x) y -> Rbar_le y (Finite z) -> is_finite y.
+Proof.
+intros x y z; destruct y; easy.
+Qed.
+
+Lemma Rplus_plus_reg_l : forall (a b c:R), b = c -> plus a b = a + c.
+Proof.
+intros. rewrite H. reflexivity.
+Qed.
+
+Lemma Rplus_plus_reg_r : forall a b c, b = c -> plus b a = c + a.
+Proof.
+intros. rewrite H. reflexivity.
+Qed.
+
+Context {E : NormedModule R_AbsRing}.
+
+Lemma norm_scal_R: forall l (x:E), norm (scal l x) = abs l * norm x.
+Proof.
+intros l x.
+apply Rle_antisym; try apply norm_scal.
+case (Req_dec l 0); intros V.
+rewrite V; unfold abs; simpl.
+rewrite Rabs_R0, Rmult_0_l.
+apply norm_ge_0.
+apply Rmult_le_reg_l with (abs (/l)).
+unfold abs; simpl.
+apply Rabs_pos_lt.
+now apply Rinv_neq_0_compat.
+apply Rle_trans with (norm x).
+rewrite <- Rmult_assoc.
+unfold abs; simpl.
+rewrite <- Rabs_mult.
+rewrite Rinv_l; trivial.
+rewrite Rabs_R1, Rmult_1_l.
+apply Rle_refl.
+apply Rle_trans with (norm (scal (/l) (scal l x))).
+right; apply f_equal.
+rewrite scal_assoc.
+apply trans_eq with (scal one x).
+apply sym_eq, scal_one.
+apply f_equal2; trivial.
+unfold one, mult; simpl.
+now field.
+apply (norm_scal (/l) (scal l x)).
+Qed.
+
+Lemma sum_n_eq_zero: forall m (L:nat -> E),
+  (forall i, (i <= m)%nat -> L i = zero) ->
+   sum_n L m = zero.
+Proof.
+intros m L H.
+apply trans_eq with (sum_n (fun n => zero) m).
+now apply sum_n_ext_loc.
+clear; induction m.
+now rewrite sum_O.
+rewrite sum_Sn, IHm.
+apply plus_zero_l.
+Qed.
+
+End RC.

LM/check_sub_structure.v

+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+Require Export Reals Coquelicot.Coquelicot.
+Require Export compatible hilbert.
+Require Export ProofIrrelevance.
+
+(** Sub-groups *)
+
+Section Subgroups.
+
+Context {G : AbelianGroup}.
+Context {P: G -> Prop}.
+Context {CCP: compatible_g P}.
+
+Record Sg:= mk_Sg {
+    val :> G ;
+    H: P val
+}.
+
+Lemma Sg_eq: forall (x y:Sg), (val x = val y) -> x = y.
+Proof.
+intros x y H.
+destruct x; destruct y.
+simpl in H.
+revert H0 H1.
+rewrite <- H.
+intros H0 H1; f_equal.
+apply proof_irrelevance.
+Qed.
+
+Definition Sg_zero : Sg := mk_Sg zero (compatible_g_zero P CCP).
+
+Definition Sg_plus (x y : Sg) : Sg :=
+    mk_Sg (plus x y)
+          (compatible_g_plus P (val x) (val y) CCP (H x) (H y)).
+
+Definition Sg_opp (x : Sg) : Sg :=
+    mk_Sg (opp x)
+          (compatible_g_opp P (val x) CCP (H x)).
+
+Lemma Sg_plus_comm: forall (x y:Sg), Sg_plus x y = Sg_plus y x.
+Proof.
+intros x y; apply Sg_eq.
+unfold Sg_plus; simpl.
+apply plus_comm.
+Qed.
+
+Lemma Sg_plus_assoc:
+  forall (x y z:Sg ), Sg_plus x (Sg_plus y z) = Sg_plus (Sg_plus x y) z.
+Proof.
+intros x y z; apply Sg_eq.
+unfold Sg_plus; simpl.
+apply plus_assoc.
+Qed.
+
+Lemma Sg_plus_zero_r: forall x:Sg, Sg_plus x Sg_zero = x.
+Proof.
+intros x; apply Sg_eq.
+unfold Sg_plus; simpl.
+apply plus_zero_r.
+Qed.
+
+Lemma Sg_plus_opp_r: forall x:Sg, Sg_plus x (Sg_opp x) = Sg_zero.
+Proof.
+intros x; apply Sg_eq.
+unfold Sg_plus; simpl.
+apply plus_opp_r.
+Qed.
+
+Definition Sg_AbelianGroup_mixin :=
+  AbelianGroup.Mixin Sg Sg_plus Sg_opp Sg_zero Sg_plus_comm
+   Sg_plus_assoc Sg_plus_zero_r Sg_plus_opp_r.
+
+Canonical Sg_AbelianGroup :=
+  AbelianGroup.Pack Sg (Sg_AbelianGroup_mixin) Sg.
+
+End Subgroups.
+
+(** Sub-modules *)
+
+Section Submodules.
+
+Context {G : ModuleSpace R_Ring}.
+Context {P: G -> Prop}.
+
+Hypothesis CPM: compatible_m P.
+
+Let Sg_Mplus := (@Sg_plus _ P (proj1 CPM)).
+
+Definition Sg_scal a (x: Sg) : (Sg):=
+    mk_Sg (scal a (val x))
+          (compatible_m_scal P a (val x) CPM (H x)).
+
+Lemma Sg_mult_one_l : forall (x : Sg), Sg_scal (@one R_Ring) x = x.
+Proof.
+intros x; apply Sg_eq.
+unfold Sg_scal; simpl.
+apply scal_one.
+Qed.
+
+Lemma Sg_mult_assoc : forall x y (f: Sg), Sg_scal x (Sg_scal y f) = Sg_scal (mult x y) f.
+Proof.
+intros x y f; apply Sg_eq.
+unfold Sg_scal; simpl.
+apply scal_assoc.
+Qed.
+
+Lemma Sg_mult_distr_l  : forall x (u v: Sg),
+  Sg_scal  x (Sg_Mplus u v) = Sg_Mplus (Sg_scal x u) (Sg_scal x v).
+Proof.
+intros x u v; apply Sg_eq.
+unfold Sg_plus; simpl.
+apply scal_distr_l.
+Qed.
+
+Lemma Sg_mult_distr_r  : forall x y u,
+  Sg_scal (plus x y) u = Sg_Mplus (Sg_scal x u) (Sg_scal y u).
+Proof.
+intros x y u; apply Sg_eq.
+unfold Sg_plus; unfold Sg_scal; simpl.
+apply scal_distr_r.
+Qed.
+
+Definition Sg_MAbelianGroup_mixin :=
+  AbelianGroup.Mixin Sg Sg_Mplus Sg_opp Sg_zero Sg_plus_comm
+   Sg_plus_assoc Sg_plus_zero_r Sg_plus_opp_r.
+
+Canonical Sg_MAbelianGroup :=
+  AbelianGroup.Pack Sg (Sg_MAbelianGroup_mixin) (@Sg _ P).
+
+Definition Sg_ModuleSpace_mixin :=
+ModuleSpace.Mixin R_Ring (Sg_MAbelianGroup)
+   _ Sg_mult_assoc Sg_mult_one_l Sg_mult_distr_l Sg_mult_distr_r.
+
+Canonical Sg_ModuleSpace :=
+  ModuleSpace.Pack R_Ring Sg (ModuleSpace.Class _ _ _ Sg_ModuleSpace_mixin) (@Sg G P).
+
+End Submodules.
+
+(** Sub-prehilbert *)
+
+Section Subprehilbert.
+
+Context {G : PreHilbert}.
+Context {P: G -> Prop}.
+Hypothesis CPM: compatible_m P.
+
+Let Sg_plus := (@Sg_plus _ P (proj1 CPM)).
+Let Sg_scal := (@Sg_scal _ P CPM).
+
+Definition Sg_inner (x y : @Sg G P) : R :=
+     (inner (val x) (val y)).
+
+Lemma Sg_inner_comm : forall (x y : Sg),
+        Sg_inner x y = Sg_inner y x.
+Proof.
+intros x y.
+apply inner_sym.
+Qed.
+
+Lemma Sg_inner_pos : forall (x : Sg),
+        0 <= Sg_inner x x.
+Proof.
+intros x.
+apply inner_ge_0.
+Qed.
+
+Lemma Sg_inner_def : forall (x : Sg),
+                           Sg_inner x x= 0 -> x = @Sg_zero G P (proj1 CPM).
+Proof.
+intros x Hx; apply Sg_eq; simpl.
+now apply inner_eq_0.
+Qed.
+
+Lemma Sg_inner_scal : forall (x y: Sg) (l : R),
+        Sg_inner (Sg_scal l x) y = l * (Sg_inner x y).
+intros x y l.
+apply inner_scal_l.
+Qed.
+
+Lemma Sg_inner_plus : forall (x y z: Sg),
+     Sg_inner (Sg_plus x y) z = plus (Sg_inner x z) (Sg_inner y z).
+Proof.
+intros x y z.
+apply inner_plus_l.
+Qed.
+
+Definition Sg_PreHilbert_mixin :=
+   PreHilbert.Mixin (@Sg_ModuleSpace G P CPM)
+       _ Sg_inner_comm Sg_inner_pos Sg_inner_def Sg_inner_scal Sg_inner_plus.
+
+Canonical Sg_PreHilbert :=
+    PreHilbert.Pack Sg (PreHilbert.Class _ _ Sg_PreHilbert_mixin) (@Sg G P).
+
+End Subprehilbert.
+
+(** Sub-hilbert *)
+
+Section Subhilbert.
+
+Context {G : Hilbert}.
+Context {P: G -> Prop}.
+
+Hypothesis CPM: compatible_m P.
+
+Let Sg_plus := (@Sg_plus _ P (proj1 CPM)).
+Let Sg_scal := (@Sg_scal _ P CPM).
+
+Definition Sg_cleanFilter (Fi : (Sg -> Prop) -> Prop) : (G -> Prop) -> Prop
+    := fun A : ((G -> Prop)) => exists V : (Sg -> Prop), Fi V /\
+           (forall f : (@Sg G P), V f -> A (val f)).
+
+Lemma Sg_cleanFilterProper: forall (Fi: (Sg -> Prop) -> Prop),
+  ProperFilter Fi -> ProperFilter (Sg_cleanFilter Fi).
+Proof.
+intros Fi (FF1,FF2).
+constructor.
+unfold Sg_cleanFilter.
+intros P0 (V,(HV1,HV2)).
+destruct (FF1 V HV1) as (f,Hf).
+specialize (HV2 f).
+exists (val f).
+apply HV2; trivial.
+constructor; unfold Sg_cleanFilter.
+exists (fun _ => True); split; try easy.
+apply FF2.
+intros P0 Q (Vp,(HP1,HP2)) (Vq,(HQ1,HQ2)).
+exists (fun x => Vp x /\ Vq x); split.
+now apply FF2.
+intros f (Hf1,Hf2).
+split.
+now apply HP2.
+now apply HQ2.
+intros P0 Q H (Vp,(HP1,HP2)).
+exists Vp; split.
+easy.
+intros f Hf.
+now apply H, HP2.
+Qed.
+
+Definition Sg_lim_v (Fi : (Sg -> Prop) -> Prop) :=
+    lim (Sg_cleanFilter Fi).
+
+End Subhilbert.

LM/compatible.v

+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+Require Export Reals Coquelicot.Coquelicot.
+
+(** AbelianGroup-compatibility *)
+
+Section AboutCompatibleG.
+
+Context {E : AbelianGroup}.
+
+Definition compatible_g (P: E -> Prop) : Prop :=
+   (forall (x y:E), P x -> P y -> P (plus x (opp y))) /\
+      (exists (x:E), P x).
+
+Lemma compatible_g_zero: forall P, compatible_g P -> P zero.
+Proof.
+intros P HP; destruct HP as (H1,(e,He)).
+specialize (H1 e e).
+rewrite plus_opp_r in H1.
+now apply H1.
+Qed.
+
+Lemma compatible_g_opp: forall P x, compatible_g P
+    -> P x -> P (opp x).
+Proof.
+intros P x HP Hx.
+rewrite <- plus_zero_l.
+apply HP; try assumption.
+now apply compatible_g_zero.
+Qed.
+
+Lemma compatible_g_plus: forall P x y, compatible_g P
+    -> P x -> P y -> P (plus x y).
+Proof.
+intros P x y HP Hx Hy.
+rewrite <- (opp_opp y).
+apply HP; try assumption.
+now apply compatible_g_opp.
+Qed.
+
+End AboutCompatibleG.
+
+(** ModuleSpace-compatibility *)
+
+Section AboutCompatibleM.
+
+Context {E : ModuleSpace R_Ring}.
+
+Definition compatible_m (phi:E->Prop):=
+  compatible_g phi /\
+  (forall (x:E) (l:R), phi x -> phi (scal l x)).
+
+Lemma compatible_m_zero: forall P, compatible_m P -> P zero.
+Proof.
+intros. destruct H.
+apply (compatible_g_zero P); trivial.
+Qed.
+
+Lemma compatible_m_plus: forall P x y, compatible_m P
+    -> P x -> P y -> P (plus x y).
+Proof.
+intros P x y Hp Hx Hy.
+destruct Hp.
+apply (compatible_g_plus P x y); trivial.
+Qed.
+
+Lemma compatible_m_scal: forall P a y, compatible_m P
+    -> P y -> P (scal a y).
+Proof.
+intros P x y HP Hy.
+apply HP; trivial.
+Qed.
+
+Lemma compatible_m_opp: forall P x, compatible_m P
+    -> P x -> P (opp x).
+Proof.
+intros. destruct H.
+apply (compatible_g_opp P); trivial.
+Qed.
+
+End AboutCompatibleM.
+
+(** Sums and direct sums  *)
+
+Section Compat_m.
+
+Context {E : ModuleSpace R_Ring}.
+
+Variable phi:E->Prop.
+Variable phi':E->Prop.
+
+Definition m_plus (phi phi':E -> Prop)
+   := (fun (x:E) => exists u u', phi u -> phi' u' -> x=plus u u').
+
+Hypothesis Cphi: compatible_m phi.
+Hypothesis Cphi': compatible_m phi'.
+
+Lemma compatible_m_plus2: compatible_m (m_plus phi phi').
+unfold compatible_m in *; unfold compatible_g in *.
+destruct Cphi as ((Cphi1,(a,Cphi2)),Cphi3).
+destruct Cphi' as ((Cphi1',(a',Cphi2')),Cphi3').
+unfold m_plus in *.
+split.
+split; intros. exists (plus x (opp y)). exists zero.
+intros. rewrite plus_zero_r. reflexivity.
+exists (plus a a'). exists a. exists a'. intros.
+reflexivity.
+intros. exists (scal l x). exists (scal zero x).
+intros. rewrite <- scal_distr_r. rewrite plus_zero_r.
+reflexivity.
+Qed.
+
+Definition direct_sumable := forall x, phi x -> phi' x -> x = zero.
+
+Lemma direct_sum_eq1:
+   direct_sumable ->
+    (forall u u' , phi u -> phi' u' -> plus u u' = zero -> u=zero /\ u'=zero).
+intros. split.
+unfold compatible_m in *.
+unfold compatible_g in *.
+assert (u = opp u').
+rewrite <- plus_opp_r with u' in H2.
+rewrite plus_comm in H2.
+apply plus_reg_l in H2.
+trivial.
+assert (phi' u).
+rewrite H3 in H2.
+rewrite H3.
+rewrite <- scal_opp_one.
+apply (proj2 Cphi'). trivial.
+apply H; trivial.
+assert (u' = opp u).
+rewrite <- plus_opp_r with u in H2.
+apply plus_reg_l in H2. trivial.
+assert (phi u').
+rewrite H3 in H2.
+rewrite H3.
+rewrite <- scal_opp_one.
+apply (proj2 Cphi). trivial.
+apply H; trivial.
+Qed.
+
+Lemma plus_u_opp_v : forall (u v : E), u = v <-> (plus u (opp v) = zero).
+intros; split.
++ intros. rewrite H. rewrite plus_opp_r. reflexivity.
++ intros. apply plus_reg_r with (opp v). rewrite plus_opp_r; trivial.
+Qed.
+
+Lemma plus_assoc_gen : forall (a b c d : E),
+     plus (plus a b) (plus c d) = plus (plus a c) (plus b d).
+intros. rewrite plus_assoc. symmetry. rewrite plus_assoc.
+assert (plus a (plus b c) = plus (plus a b) c).
+apply plus_assoc.
+assert (plus a (plus c b) = plus (plus a c) b).
+apply plus_assoc.
+rewrite <- H; rewrite <-H0.
+rewrite (plus_comm c b). reflexivity.
+Qed.
+
+Lemma direct_sum_eq2:
+  (forall u u' , phi u -> phi' u' -> plus u u' = zero -> u=zero /\ u'=zero) ->
+   (forall u v u' v', phi u -> phi v -> phi' u' -> phi' v' -> plus u u' = plus v v' -> u=v /\ u'=v').
+intros. unfold compatible_m in *; unfold compatible_g in *.
+destruct Cphi as ((Cphi1,(x,Cphi2)),Cphi3).
+destruct Cphi' as ((Cphi'1,(x',Cphi'2)),Cphi'3).
+assert (plus (plus u (opp v)) (plus u' (opp v')) = zero).
+rewrite plus_assoc_gen. rewrite H4.
+rewrite plus_assoc_gen. rewrite plus_opp_r. rewrite plus_opp_r.
+rewrite plus_zero_r. reflexivity.
+rewrite plus_u_opp_v.
+rewrite (plus_u_opp_v u' v').
+apply H.
+apply Cphi1; trivial.
+apply Cphi'1; trivial.
+trivial.
+Qed.
+
+Lemma direct_sum_eq3:
+   (forall u v u' v', phi u -> phi v -> phi' u' -> phi' v' -> plus u u' = plus v v' -> u=v /\ u'=v')
+     -> direct_sumable.
+intros.
+unfold compatible_m in *; unfold compatible_g in *; unfold direct_sumable.
+intros.
+destruct Cphi as ((Cphi1,(y,Cphi2)),Cphi3).
+destruct Cphi' as ((Cphi'1,(y',Cphi'2)),Cphi'3).
+apply (Cphi3 y zero) in Cphi2.
+apply (Cphi'3 y' zero) in Cphi'2.
+apply (Cphi'3 x (opp one)) in H1.
+assert ((x = zero) /\ (opp x = zero)).
+apply H. trivial. rewrite <- (scal_zero_l y). trivial.
+rewrite <- scal_opp_one. trivial.
+rewrite <- (scal_zero_l y'). trivial.
+rewrite plus_opp_r.
+rewrite plus_zero_l. reflexivity.
+intuition.
+Qed.
+
+End Compat_m.

LM/lax_milgram_cea.v

+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+Require Import hilbert.
+Require Export Decidable.
+Require Export FunctionalExtensionality.
+Require Export mathcomp.ssreflect.ssreflect.
+Require Export Coquelicot.Hierarchy.
+Require Export Reals.
+Require Export logic_tricks.
+Require Export ProofIrrelevanceFacts.
+Require Export lax_milgram.
+
+(** Lax-Milgram-Cea's Theorem *)
+
+Section LMC.
+
+Context { E : Hilbert }.
+
+Variable a : E -> E -> R.
+Variable M : R.
+Variable alpha : R.
+Hypothesis Hba : is_bounded_bilinear_mapping a M.
+Hypothesis Hca : is_coercive a alpha.
+
+Lemma Galerkin_orthogonality (u uh : E)
+               (f:topo_dual E) (phi : E -> Prop) :
+      (forall (f : topo_dual E), decidable (exists u : E, f u <> 0)) ->
+      phi uh ->
+      is_sol_linear_pb_phi a (fun x:E => True) f u ->
+      is_sol_linear_pb_phi a phi f uh ->
+      (forall vh : E, phi vh -> a (minus u uh) vh = 0).
+Proof.
+intros Hd phi_uh Hle Hleh vh SubEh.
+unfold minus.
+destruct Hba as ((Hba1,(Hba2,(Hba3,Hba4))),_).
+rewrite Hba3.
+replace (opp uh) with (scal (opp one) uh).
+rewrite Hba1.
+rewrite scal_opp_one.
+unfold is_sol_linear_pb_phi in Hle.
+destruct Hle as (_,Hle).
+rewrite Hle.
+rewrite (proj2 Hleh).
+rewrite plus_opp_r.
+reflexivity.
+trivial.
+trivial.
+rewrite scal_opp_one.
+reflexivity.
+Qed.
+
+Lemma Lax_Milgram_Cea (u uh : E) (f:topo_dual E)  (phi : E -> Prop) :
+      (forall (f : topo_dual E), decidable (exists u : E, f u <> 0)) ->
+      phi uh -> compatible_m phi -> my_complete phi ->
+      is_sol_linear_pb_phi a (fun x:E => True) f u ->
+      is_sol_linear_pb_phi a phi f uh -> (forall vh : E, phi vh ->
+      norm (minus u uh) <= (M/alpha) * norm (minus u vh)).
+Proof.
+intros Hdf Huh HM HC H1 H2 vh Hvh.
+destruct (is_zero_dec (minus u uh)).
+rewrite H.
+rewrite norm_zero.
+apply Rmult_le_pos.
+destruct Hba as (_,(Hb,_)).
+replace (M / alpha) with (M * / alpha); try trivial.
+replace 0 with (0*0).
+apply Rmult_le_compat; intuition.
+intuition.
+destruct Hca as (Hc,_).
+apply Rinv_0_lt_compat in Hc.
+intuition. ring.
+apply norm_ge_0.
+assert (Ha : a (minus u uh) (minus u vh) = a (minus u uh) u).
+transitivity (minus (a (minus u uh) u) (a (minus u uh) vh)).
+destruct Hba as ((Hba1,(Hba2,(Hba3,Hba4))),_).
+rewrite Hba4.
+unfold minus at 3.
+replace (a (minus u uh) (opp vh)) with (opp (a (minus u uh) vh)).
+reflexivity.
+replace (opp vh) with (scal (opp one) vh).
+rewrite Hba2.
+rewrite scal_opp_one.
+reflexivity.
+rewrite scal_opp_one.
+reflexivity.
+replace (a (minus u uh) vh) with 0.
+unfold minus at 1.
+rewrite opp_zero.
+rewrite plus_zero_r.
+reflexivity.
+symmetry.
+apply Galerkin_orthogonality with f phi; try assumption.
+apply Rmult_le_reg_l with alpha.
+apply Hca.
+field_simplify.
+replace (alpha * norm (minus u uh) / 1) with (alpha * norm (minus u uh))
+        by field.
+replace (M * norm (minus u vh) / 1) with (M * norm (minus u vh)) by field.
+apply Rmult_le_reg_r with (norm (minus u uh)).
+now apply norm_gt_0.
+unfold is_bounded_bilinear_mapping in Hba.
+destruct Hba as (H0,H3).
+unfold is_bounded_bi in H3.
+destruct H3 as (H3,H4).
+specialize (H4 (minus u uh) (minus u vh)).
+apply Rle_trans with (norm (a (minus u uh) (minus u vh)));
+      try assumption.
+rewrite Ha.
+destruct Hca as (H5,H6).
+unfold is_sol_linear_pb_phi in *.
+destruct H1 as (X1,H1).
+destruct H2 as (X2,H2).
+replace (a (minus u uh) u)
+        with (a (minus u uh) (minus u uh)).
+specialize (H6 (minus u uh)).
+unfold norm at 3.
+simpl.
+apply Rle_trans with (a (minus u uh) (minus u uh)).
+trivial.
+unfold abs.
+simpl.
+apply Rle_abs.
+destruct H0 as (H0,H7).
+destruct H7 as (H7,(H8,H9)).
+unfold minus.
+rewrite H9.
+replace (a (plus u (opp uh)) u) with
+        (plus (a (plus u (opp uh)) u) 0).
+f_equal.
+now rewrite plus_zero_r.
+specialize (H1 uh).
+apply H1 in X1.
+specialize (H2 uh).
+apply H2 in X2.
+clear H1 H2.
+rewrite H8.
+replace (a u (opp uh)) with (opp (a u uh)).
+rewrite X1.
+replace (a (opp uh) (opp uh)) with (a uh uh).
+rewrite X2.
+rewrite plus_opp_l; reflexivity.
+replace (opp uh) with (scal (opp one) uh).
+replace (opp uh) with (scal (opp one) uh).
+rewrite H0 H7 2!scal_opp_l scal_one opp_opp scal_one.
+reflexivity.
+rewrite scal_opp_one.
+reflexivity.
+rewrite scal_opp_one; reflexivity.
+replace (opp uh) with (scal (opp one) uh).
+rewrite H7 scal_opp_one.
+reflexivity.
+rewrite scal_opp_one.
+reflexivity.
+rewrite plus_zero_r; reflexivity.
+replace (M * norm (minus u vh) * norm (minus u uh)) with
+        (M * norm (minus u uh) * norm (minus u vh)) by ring.
+assumption.
+destruct Hca.
+intro Hk.
+rewrite Hk in H0.
+absurd (0 < 0); try assumption.
+exact (Rlt_irrefl 0).
+Qed.
+
+End LMC.

LM/logic_tricks.v

+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+Require Import Decidable.
+Require Import Arith.
+
+(** Intuitionistic tricks for decidability *)
+
+Section LT.
+
+Lemma logic_not_not : forall Q, False <-> ((Q \/~Q) -> False).
+split.
+now intros H H'.
+intros H'.
+apply H'.
+right.
+intros H.
+apply H'.
+now left.
+Qed.
+
+Lemma logic_notex_forall (T : Type) :
+  forall (P : T -> Prop) (x : T),
+ (forall x, P x) -> (~ exists x, ~ P x).
+Proof.
+intros P x H.
+intro H0.
+destruct H0 as (t,H0).
+apply H0.
+apply H.
+Qed.
+
+Lemma logic_dec_notnot (T : Type) :
+  forall P : T -> Prop, forall x : T,
+    (decidable (P x)) -> (P x <-> ~~ P x).
+Proof.
+intros P x Dec.
+split.
++ intro H.
+  intuition.
++ intro H.
+  unfold decidable in Dec.
+  destruct Dec.
+  trivial.
+  exfalso.
+  apply H.
+  exact H0.
+Qed.
+
+Lemma decidable_ext: forall P Q, decidable P -> (P <->Q) -> decidable Q.
+Proof.
+intros P Q HP (H1,H2).
+case HP; intros HP'.
+left; now apply H1.
+right; intros HQ.
+now apply HP', H2.
+Qed.
+
+Lemma decidable_ext_aux: forall (T : Type), forall P1 P2 Q,
+  decidable (exists w:T, P1 w  /\ Q w) ->
+    (forall x, P1 x <-> P2 x) ->
+      decidable (exists w, P2 w  /\ Q w).
+Proof.
+intros T P1 P2 Q H H1.
+case H.
+intros (w,(Hw1,Hw2)).
+left; exists w; split; try assumption.
+now apply H1.
+intros H2; right; intros (w,(Hw1,Hw2)).
+apply H2; exists w; split; try assumption.
+now apply H1.
+Qed.
+
+Lemma decidable_and: forall (T : Type), forall P1 P2 (w : T),
+   decidable (P1 w) -> decidable (P2 w) -> decidable (P1 w /\ P2 w).
+Proof.
+intros T P1 P2 w H1 H2.
+unfold decidable.
+destruct H1.
+destruct H2.
+left; intuition.
+right.
+intro.
+now apply H0.
+destruct H2.
+right.
+intro.
+now apply H.
+right.
+intro.
+now apply H.
+Qed.
+
+(** Strong induction *)
+
+Theorem strong_induction:
+ forall P : nat -> Prop,
+    (forall n : nat, (forall k : nat, ((k < n)%nat -> P k)) -> P n) ->
+       forall n : nat, P n.
+Proof.
+intros P H n.
+assert (forall k, (k < S n)%nat -> P k).
+induction n.
+intros k Hk.
+replace k with 0%nat.
+apply H.
+intros m Hm; contradict Hm.
+apply lt_n_0.
+generalize Hk; case k; trivial.
+intros m Hm; contradict Hm.
+apply le_not_lt.
+now auto with arith.
+intros k Hk.
+apply H.
+intros m Hm.
+apply IHn.
+apply lt_le_trans with (1:=Hm).
+now apply gt_S_le.
+apply H0.
+apply le_n.
+Qed.
+
+(** Equivalent definition for existence + uniqueness *)
+
+Lemma unique_existence1: forall (A : Type) (P : A -> Prop),
+     (exists x : A, P x) /\ uniqueness P -> (exists ! x : A, P x).
+Proof.
+intros A P.
+apply unique_existence.
+Qed.
+
+End LT.

Lebesgue/.config.profile

+DEPS="\
+    logic_compl.v\
+    subset_compl.v\
+    list_compl.v\
+    R_compl.v\
+    sort_compl.v\
+    Rbar_compl.v\
+    UniformSpace_compl.v\
+\
+    countable_sets.v\
+    topo_bases_R.v\
+    sum_Rbar_nonneg.v\
+\
+    sigma_algebra.v\
+    sigma_algebra_R_Rbar.v\
+    measurable_fun.v\
+    measure.v\
+\
+    simple_fun.v\
+    LInt_p.v\
+"