diff options
Diffstat (limited to 'test-suite')
28 files changed, 1029 insertions, 38 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 37091a49e5..111bd52a33 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -38,14 +38,15 @@ LIB := .. BIN := $(shell cd ..; pwd)/bin/ COQFLAGS?= -coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite $(COQFLAGS) +coqc_boot := $(BIN)coqc -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite $(COQFLAGS) coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite $(COQFLAGS) coqchk := $(BIN)coqchk -coqlib $(LIB) -R prerequisite TestSuite coqdoc := $(BIN)coqdoc +coqtop := $(BIN)coqtop -batch -coqlib $(LIB) -boot -q -test-mode -R prerequisite TestSuite coqtopbyte := $(BIN)coqtop.byte -coqtopload := $(coqtop) -async-proofs-cache force -load-vernac-source -coqtopcompile := $(coqtop) -async-proofs-cache force -compile +coqc_interactive := $(coqc) -async-proofs-cache force +coqc_boot_interactive := $(coqc_boot) -async-proofs-cache force coqdep := $(BIN)coqdep -coqlib $(LIB) VERBOSE?= @@ -60,12 +61,8 @@ SINGLE_QUOTE=" #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter # wrap the arguments in parens, but only if they exist get_coq_prog_args_in_parens = $(subst $(SINGLE_QUOTE),,$(if $(call get_coq_prog_args,$(1)), ($(call get_coq_prog_args,$(1))))) -# get the command to use with this set of arguments; if there's -compile, use coqc, else use coqtop -has_profile_ltac_or_compile_flag = $(filter "-profile-ltac-cutoff" "-profile-ltac" "-compile",$(call get_coq_prog_args,$(1))) -get_command_based_on_flags = $(if $(call has_profile_ltac_or_compile_flag,$(1)),$(coqtopcompile),$(coqtopload)) get_set_impredicativity= $(filter "-impredicative-set",$(call get_coq_prog_args,$(1))) - bogomips:= ifneq (,$(wildcard /proc/cpuinfo)) sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc @@ -209,7 +206,7 @@ $(addsuffix .log,$(wildcard bugs/opened/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...still active"; \ @@ -231,7 +228,7 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -297,7 +294,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ echo " $<...could not be prepared" ; \ @@ -316,7 +313,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v)): %.v $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods)"; \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") $$opts 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -342,7 +339,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ $$opts 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ @@ -367,7 +364,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ @@ -392,7 +389,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ output=$*.out.real; \ - $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ @@ -431,7 +428,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out echo $(call log_intro,$<); \ tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \ tmpexpected=`mktemp /tmp/coqcheck.XXXXXX`; \ - $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \ + $(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \ | grep -v "Welcome to Coq" \ | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ @@ -486,7 +483,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) $(HIDE){ \ echo $(call log_intro,$<); \ true "extract effective user time"; \ - res=`$(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \ + res=`$(coqc_boot_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 | sed -n -e "s/Finished transaction in .*(\([0-9]*\.[0-9]*\)u.*)/\1/p" | head -1`; \ R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_failure); \ @@ -517,7 +514,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ - $(coqtopcompile) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ + $(coqc) "$<" $(call get_coq_prog_args,"$<") 2>&1; R=$$?; times; \ if [ $$R != 0 ]; then \ echo $(log_success); \ echo " $<...still wished"; \ @@ -531,7 +528,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG # Additional dependencies for module tests $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo modules/%.vo: modules/%.v - $(HIDE)$(coqtop) -R modules Mods -compile $< + $(HIDE)$(coqc) -R modules Mods $< ####################################################################### # Miscellaneous tests @@ -550,7 +547,7 @@ $(patsubst %.sh,%.log,$(wildcard misc/*.sh)): %.log: %.sh $(PREREQUISITELOG) echo $(call log_intro,$<); \ export BIN="$(BIN)"; \ export coqc="$(coqc)"; \ - export coqtop="$(coqtop)"; \ + export coqtop="$(coqc_boot)"; \ export coqdep="$(coqdep)"; \ export coqtopbyte="$(coqtopbyte)"; \ "$<" 2>&1; R=$$?; times; \ @@ -591,7 +588,7 @@ vio: $(patsubst %.v,%.vio.log,$(wildcard vio/*.v)) @echo "TEST $<" $(HIDE){ \ $(coqc) -quick -R vio vio $* 2>&1 && \ - $(coqtop) -R vio vio -vio2vo $*.vio 2>&1 && \ + $(coqc) -R vio vio -vio2vo $*.vio 2>&1 && \ $(coqchk) -R vio vio -norec $(subst /,.,$*) 2>&1; \ if [ $$? = 0 ]; then \ echo $(log_success); \ diff --git a/test-suite/bugs/closed/bug_4836.v b/test-suite/bugs/closed/bug_4836.v index 5838dcd8a7..9aefb10172 100644 --- a/test-suite/bugs/closed/bug_4836.v +++ b/test-suite/bugs/closed/bug_4836.v @@ -1 +1 @@ -(* -*- coq-prog-args: ("-compile" "bugs/closed/PLACEHOLDER.v") -*- *) +(* -*- coq-prog-args: ("bugs/closed/PLACEHOLDER.v") -*- *) diff --git a/test-suite/bugs/closed/bug_7811.v b/test-suite/bugs/closed/bug_7811.v index fee330f22d..155f3285b7 100644 --- a/test-suite/bugs/closed/bug_7811.v +++ b/test-suite/bugs/closed/bug_7811.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *) +(* -*- mode: coq; coq-prog-args: ("-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *) (* File reduced by coq-bug-finder from original input, then from 140 lines to 26 lines, then from 141 lines to 27 lines, then from 142 lines to 27 lines, then from 272 lines to 61 lines, then from 291 lines to 94 lines, then from 678 lines to 142 lines, then from 418 lines to 161 lines, then from 538 lines to 189 lines, then from 840 lines to 493 lines, then from 751 lines to 567 lines, then from 913 lines to 649 lines, then from 875 lines to 666 lines, then from 784 lines to 568 lines, then from 655 lines to 173 lines, then from 317 lines to 94 lines, then from 172 lines to 86 lines, then from 102 lines to 86 lines, then from 130 lines to 86 lines, then from 332 lines to 112 lines, then from 279 lines to 111 lines, then from 3996 lines to 5697 lines, then from 153 lines to 117 lines, then from 146 lines to 108 lines, then from 124 lines to 108 lines *) (* coqc version 8.8.0 (May 2018) compiled on May 2 2018 16:49:46 with OCaml 4.02.3 coqtop version 8.8.0 (May 2018) *) diff --git a/test-suite/bugs/closed/bug_9268.v b/test-suite/bugs/closed/bug_9268.v new file mode 100644 index 0000000000..02dd46f6d2 --- /dev/null +++ b/test-suite/bugs/closed/bug_9268.v @@ -0,0 +1,46 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. + +Local Open Scope Z_scope. + +Definition Register := Z%type. + +Definition Opcode := Z%type. + +Inductive InstructionI : Type + := Lb : Register -> Register -> Z -> InstructionI + | InvalidI : InstructionI. + +Inductive Instruction : Type + := IInstruction : InstructionI -> Instruction. + +Definition funct3_LB : Z := 0. + +Definition opcode_LOAD : Opcode := 3. + +Set Universe Polymorphism. + +Definition MachineInt := Z. + +Definition funct3_JALR := 0. + +Axiom InstructionMapper: Type -> Type. + +Definition apply_InstructionMapper(mapper: InstructionMapper Z)(inst: Instruction): Z := + match inst with + | IInstruction InvalidI => 2 + | IInstruction (Lb rd rs1 oimm12) => 3 + end. + +Axiom Encoder: InstructionMapper MachineInt. + +Definition encode: Instruction -> MachineInt := apply_InstructionMapper Encoder. + +Lemma foo: forall (ins: InstructionI), + 0 <= encode (IInstruction ins) -> + 0 <= encode (IInstruction ins) . +Proof. + Set Printing Universes. + intros. + lia. +Qed. diff --git a/test-suite/bugs/closed/bug_9451.v b/test-suite/bugs/closed/bug_9451.v new file mode 100644 index 0000000000..03bb0433f1 --- /dev/null +++ b/test-suite/bugs/closed/bug_9451.v @@ -0,0 +1,8 @@ +Goal False. +cut True. +assert False. +evar (x : True). +let v := open_constr:(_) in idtac. all: exfalso; clear. +Optimize Proof. +(* Error: Anomaly "grounding a non evar-free term" *) +Abort All. diff --git a/test-suite/complexity/constructor.v b/test-suite/complexity/constructor.v index c5e1953829..31217ca75e 100644 --- a/test-suite/complexity/constructor.v +++ b/test-suite/complexity/constructor.v @@ -214,3 +214,4 @@ Fixpoint expand (n : nat) : Prop := Example Expand : expand 2500. Time constructor. (* ~0.45 secs *) +Qed. diff --git a/test-suite/complexity/f_equal.v b/test-suite/complexity/f_equal.v index 86698fa872..c2c566930b 100644 --- a/test-suite/complexity/f_equal.v +++ b/test-suite/complexity/f_equal.v @@ -12,3 +12,4 @@ end. Goal stupid 23 = stupid 23. Timeout 5 Time f_equal. +Abort. diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index a76fa19d3c..298a07c1c4 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -111,3 +111,4 @@ Lemma test: forall n1 w1 n2 w2, mk_world n1 w1 = mk_world n2 w2 -> Proof. intros. Timeout 10 Time injection H. +Abort. diff --git a/test-suite/complexity/ring.v b/test-suite/complexity/ring.v index 51f7c4dabc..2d585ce5c5 100644 --- a/test-suite/complexity/ring.v +++ b/test-suite/complexity/ring.v @@ -5,3 +5,4 @@ Require Import ZArith. Open Scope Z_scope. Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13. Timeout 5 Time intro; ring. +Abort. diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v index 04fa59075b..1c119b8e42 100644 --- a/test-suite/complexity/ring2.v +++ b/test-suite/complexity/ring2.v @@ -50,3 +50,4 @@ Infix "+" := Zadd : Z_scope. Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13. Timeout 5 Time intro; ring. +Abort. diff --git a/test-suite/complexity/setoid_rewrite.v b/test-suite/complexity/setoid_rewrite.v index 2e3b006ef0..10b270ccad 100644 --- a/test-suite/complexity/setoid_rewrite.v +++ b/test-suite/complexity/setoid_rewrite.v @@ -8,3 +8,4 @@ Variable f : nat -> Prop. Goal forall U:Prop, f 100 <-> U. intros U. Timeout 5 Time setoid_replace U with False. +Abort. diff --git a/test-suite/complexity/unification.v b/test-suite/complexity/unification.v index d2ea527516..0c9915c84e 100644 --- a/test-suite/complexity/unification.v +++ b/test-suite/complexity/unification.v @@ -49,3 +49,4 @@ Goal )))) . Timeout 2 Time try refine (refl_equal _). +Abort. diff --git a/test-suite/coqchk/inductive_functor_squash.v b/test-suite/coqchk/inductive_functor_squash.v new file mode 100644 index 0000000000..9d33fafc4c --- /dev/null +++ b/test-suite/coqchk/inductive_functor_squash.v @@ -0,0 +1,15 @@ + + +Module Type T. + Parameter f : nat -> Type. +End T. + +Module F(A:T). + Inductive ind : Prop := + C : A.f 0 -> ind. +End F. + +Module A. Definition f (x:nat) := True. End A. + +Module M := F A. +(* M.ind could eliminate into Set/Type even though F.ind can't *) diff --git a/test-suite/misc/4722.sh b/test-suite/misc/4722.sh index 86bc50b5cd..70071b9d60 100755 --- a/test-suite/misc/4722.sh +++ b/test-suite/misc/4722.sh @@ -4,12 +4,12 @@ set -e # create test files mkdir -p misc/4722 ln -sf toto misc/4722/tata -touch misc/4722.v +touch misc/bug_4722.v # run test -$coqtop "-R" "misc/4722" "Foo" -top Top -load-vernac-source misc/4722.v +$coqc "-R" "misc/4722" "Foo" -top Top misc/bug_4722.v # clean up test files rm misc/4722/tata rmdir misc/4722 -rm misc/4722.v +rm misc/bug_4722.v diff --git a/test-suite/misc/7704.sh b/test-suite/misc/7704.sh index 0ca2c97d24..5fc171649e 100755 --- a/test-suite/misc/7704.sh +++ b/test-suite/misc/7704.sh @@ -4,4 +4,4 @@ set -e export PATH=$BIN:$PATH -${coqtop#"$BIN"} -compile misc/aux7704.v +${coqc#"$BIN"} misc/aux7704.v diff --git a/test-suite/misc/aux7704.v b/test-suite/misc/aux7704.v index 6fdcf67684..1c95211a71 100644 --- a/test-suite/misc/aux7704.v +++ b/test-suite/misc/aux7704.v @@ -1,4 +1,3 @@ - Goal True /\ True. Proof. split. diff --git a/test-suite/misc/deps-checksum.sh b/test-suite/misc/deps-checksum.sh index a15a8fbee9..8523358303 100755 --- a/test-suite/misc/deps-checksum.sh +++ b/test-suite/misc/deps-checksum.sh @@ -3,4 +3,4 @@ rm -f misc/deps/A/*.vo misc/deps/B/*.vo $coqc -R misc/deps/A A misc/deps/A/A.v $coqc -R misc/deps/B A misc/deps/B/A.v $coqc -R misc/deps/B A misc/deps/B/B.v -$coqtop -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v +$coqc -R misc/deps/B A -R misc/deps/A A misc/deps/checksum.v diff --git a/test-suite/misc/deps-order.sh b/test-suite/misc/deps-order.sh index 6bb2ba2da0..551515b0d6 100755 --- a/test-suite/misc/deps-order.sh +++ b/test-suite/misc/deps-order.sh @@ -10,12 +10,12 @@ R=$? times $coqc -R misc/deps/lib lib misc/deps/lib/foo.v 2>&1 $coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/foo.v 2>&1 -$coqtop -R misc/deps/lib lib -R misc/deps/client client -load-vernac-source misc/deps/client/bar.v 2>&1 +$coqc -R misc/deps/lib lib -R misc/deps/client client misc/deps/client/bar.v 2>&1 S=$? if [ $R = 0 ] && [ $S = 0 ]; then - printf "coqdep and coqtop agree\n" + printf "coqdep and coqc agree\n" exit 0 else - printf "coqdep and coqtop disagree\n" + printf "coqdep and coqc disagree\n" exit 1 fi diff --git a/test-suite/misc/deps-utf8.sh b/test-suite/misc/deps-utf8.sh index acb45b2292..af69370ce4 100755 --- a/test-suite/misc/deps-utf8.sh +++ b/test-suite/misc/deps-utf8.sh @@ -8,7 +8,7 @@ rm -f misc/deps/théorèmes/*.v tmpoutput=$(mktemp /tmp/coqcheck.XXXXXX) $coqc -R misc/deps AlphaBêta misc/deps/αβ/γδ.v R=$? -$coqtop -R misc/deps AlphaBêta -load-vernac-source misc/deps/αβ/εζ.v +$coqc -R misc/deps AlphaBêta misc/deps/αβ/εζ.v S=$? if [ $R = 0 ] && [ $S = 0 ]; then exit 0 diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v index 7658ce718e..440fe46003 100644 --- a/test-suite/output/FunExt.v +++ b/test-suite/output/FunExt.v @@ -1,3 +1,4 @@ +(* -*- coq-prog-args: ("-async-proofs" "no") -*- *) Require Import FunctionalExtensionality. (* Basic example *) diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 72d5a9253a..7a64b7eb45 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -50,4 +50,4 @@ myAnd1 True True r 2 3 : Prop Notation Cn := Foo.FooCn -Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn +Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v index cd667bbd00..a53b52396f 100644 --- a/test-suite/output/RecognizePluginWarning.v +++ b/test-suite/output/RecognizePluginWarning.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *) +(* -*- mode: coq; coq-prog-args: ("-w" "extraction-logical-axiom") -*- *) (* Test that mentioning a warning defined in plugins works. The failure mode here is that these result in a warning about unknown warnings, since the diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v index 60faac8dd9..c875051bdc 100644 --- a/test-suite/output/Show.v +++ b/test-suite/output/Show.v @@ -5,7 +5,7 @@ Theorem nums : forall (n m : nat), n = m -> (S n) = (S m). Proof. intros. - induction n as [| n']. + induction n as [| n']. induction m as [| m']. Show. Admitted. diff --git a/test-suite/output/UnclosedBlocks.v b/test-suite/output/UnclosedBlocks.v index 854bd6a6d5..b9ba579246 100644 --- a/test-suite/output/UnclosedBlocks.v +++ b/test-suite/output/UnclosedBlocks.v @@ -1,4 +1,3 @@ -(* -*- mode: coq; coq-prog-args: ("-compile" "UnclosedBlocks.v") *) Module Foo. Module Closed. End Closed. diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v index c6e0054641..618b8fd42f 100644 --- a/test-suite/output/UsePluginWarning.v +++ b/test-suite/output/UsePluginWarning.v @@ -1,5 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *) - +(* -*- mode: coq; coq-prog-args: ("-w" "-extraction-logical-axiom") -*- *) Require Extraction. Axiom foo : Prop. diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v index 5f1926f142..5f7e3ab9dd 100644 --- a/test-suite/output/simpl.v +++ b/test-suite/output/simpl.v @@ -11,3 +11,4 @@ Undo. simpl (0 + _). Show. Undo. +Abort. diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v index 179dec3fb0..c987d66c5f 100644 --- a/test-suite/output/unifconstraints.v +++ b/test-suite/output/unifconstraints.v @@ -1,3 +1,4 @@ +(* -*- coq-prog-args: ("-async-proofs" "no") -*- *) (* Set Printing Existential Instances. *) Unset Solve Unification Constraints. Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat. diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v new file mode 100644 index 0000000000..62ecece792 --- /dev/null +++ b/test-suite/success/Nia.v @@ -0,0 +1,918 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Open Scope Z_scope. + +(** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this + file. *) +Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.to_euclidean_division_equations. + +Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed. +Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed. + +Ltac unique_pose_proof pf := + let T := type of pf in + lazymatch goal with + | [ H : T |- _ ] => fail + | _ => pose proof pf + end. + +Ltac saturate_mod_div := + repeat match goal with + | [ |- context[?x mod ?y] ] => unique_pose_proof (Z_zerop_or (x / y)) + | [ H : context[?x mod ?y] |- _ ] => unique_pose_proof (Z_zerop_or (x / y)) + | [ |- context[?x / ?y] ] => unique_pose_proof (Z_zerop_or y) + | [ H : context[?x / ?y] |- _ ] => unique_pose_proof (Z_zerop_or y) + | [ |- context[Z.rem ?x ?y] ] => unique_pose_proof (Z_zerop_or (Z.quot x y)) + | [ H : context[Z.rem ?x ?y] |- _ ] => unique_pose_proof (Z_zerop_or (Z.quot x y)) + | [ |- context[Z.quot ?x ?y] ] => unique_pose_proof (Z_zerop_or y) + | [ H : context[Z.quot ?x ?y] |- _ ] => unique_pose_proof (Z_zerop_or y) + end. + +Ltac t := intros; saturate_mod_div; try nia. + +Ltac destr_step := + match goal with + | [ H : and _ _ |- _ ] => destruct H + | [ H : or _ _ |- _ ] => destruct H + end. + +Example mod_0_l: forall x : Z, 0 mod x = 0. Proof. t. Qed. +Example mod_0_r: forall x : Z, x mod 0 = 0. Proof. intros; nia. Qed. +Example Z_mod_same_full: forall a : Z, a mod a = 0. Proof. t. Qed. +Example Zmod_0_l: forall a : Z, 0 mod a = 0. Proof. t. Qed. +Example Zmod_0_r: forall a : Z, a mod 0 = 0. Proof. intros; nia. Qed. +Example mod_mod_same: forall x y : Z, (x mod y) mod y = x mod y. Proof. t. Qed. +Example Zmod_mod: forall a n : Z, (a mod n) mod n = a mod n. Proof. t. Qed. +Example Zmod_1_r: forall a : Z, a mod 1 = 0. Proof. intros; nia. Qed. +Example Zmod_div: forall a b : Z, a mod b / b = 0. Proof. intros; nia. Qed. +Example Z_mod_1_r: forall a : Z, a mod 1 = 0. Proof. intros; nia. Qed. +Example Z_mod_same: forall a : Z, a > 0 -> a mod a = 0. Proof. t. Qed. +Example Z_mod_mult: forall a b : Z, (a * b) mod b = 0. +Proof. + intros a b. + assert (b = 0 \/ (a * b) / b = a) by nia. + nia. +Qed. +Example Z_mod_same': forall a : Z, a <> 0 -> a mod a = 0. Proof. t. Qed. +Example Z_mod_0_l: forall a : Z, a <> 0 -> 0 mod a = 0. Proof. t. Qed. +Example Zmod_opp_opp: forall a b : Z, - a mod - b = - (a mod b). +Proof. + intros a b. + pose proof (Z_eq_dec_or ((-a)/(-b)) (a/b)). + nia. +Qed. +Example Z_mod_le: forall a b : Z, 0 <= a -> 0 < b -> a mod b <= a. Proof. t. Qed. +Example Zmod_le: forall a b : Z, 0 < b -> 0 <= a -> a mod b <= a. Proof. t. Qed. +Example Zplus_mod_idemp_r: forall a b n : Z, (b + a mod n) mod n = (b + a) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((b + a mod n) / n = (b / n) + (b mod n + a mod n) / n) + by nia. + assert ((b + a) / n = (b / n) + (a / n) + (b mod n + a mod n) / n) + by nia. + nia. +Qed. +Example Zplus_mod_idemp_l: forall a b n : Z, (a mod n + b) mod n = (a + b) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a mod n + b) / n = (b / n) + (b mod n + a mod n) / n) by nia. + assert ((a + b) / n = (b / n) + (a / n) + (b mod n + a mod n) / n) by nia. + nia. +Qed. +Example Zmult_mod_distr_r: forall a b c : Z, (a * c) mod (b * c) = a mod b * c. +Proof. + intros a b c. + destruct (Z_zerop c); try nia. + pose proof (Z_eq_dec_or ((a * c) / (b * c)) (a / b)). + nia. +Qed. +Example Z_mod_zero_opp_full: forall a b : Z, a mod b = 0 -> - a mod b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or (a/b) (-(-a/b))). + nia. +Qed. +Example Zmult_mod_idemp_r: forall a b n : Z, (b * (a mod n)) mod n = (b * a) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((b * (a mod n)) / n = (b / n) * (a mod n) + ((b mod n) * (a mod n)) / n) + by nia. + assert ((b * a) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((b mod n) * (a mod n)) / n) + by nia. + nia. +Qed. +Example Zmult_mod_idemp_l: forall a b n : Z, (a mod n * b) mod n = (a * b) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert (((a mod n) * b) / n = (b / n) * (a mod n) + ((b mod n) * (a mod n)) / n) + by nia. + assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((b mod n) * (a mod n)) / n) + by nia. + nia. +Qed. +Example Zminus_mod_idemp_r: forall a b n : Z, (a - b mod n) mod n = (a - b) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a - b mod n) / n = a / n + ((a mod n) - (b mod n)) / n) by nia. + assert ((a - b) / n = a / n - b / n + ((a mod n) - (b mod n)) / n) by nia. + nia. +Qed. +Example Zminus_mod_idemp_l: forall a b n : Z, (a mod n - b) mod n = (a - b) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a mod n - b) / n = - (b / n) + ((a mod n) - (b mod n)) / n) by nia. + assert ((a - b) / n = a / n - b / n + ((a mod n) - (b mod n)) / n) by nia. + nia. +Qed. +Example Z_mod_plus_full: forall a b c : Z, (a + b * c) mod c = a mod c. +Proof. + intros a b c. + pose proof (Z_eq_dec_or ((a+b*c)/c) (a/c + b)). + nia. +Qed. +Example Zmult_mod_distr_l: forall a b c : Z, (c * a) mod (c * b) = c * (a mod b). +Proof. + intros a b c. + destruct (Z_zerop c); try nia. + pose proof (Z_eq_dec_or ((c * a) / (c * b)) (a / b)). + nia. +Qed. +Example Z_mod_zero_opp_r: forall a b : Z, a mod b = 0 -> a mod - b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or (a/b) (-(a/-b))). + nia. +Qed. +Example Zmod_1_l: forall a : Z, 1 < a -> 1 mod a = 1. Proof. t. Qed. +Example Z_mod_1_l: forall a : Z, 1 < a -> 1 mod a = 1. Proof. t. Qed. +Example Z_mod_mul: forall a b : Z, b <> 0 -> (a * b) mod b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or ((a*b)/b) a). + nia. +Qed. +Example Zminus_mod: forall a b n : Z, (a - b) mod n = (a mod n - b mod n) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a - b) / n = (a / n) - (b / n) + ((a mod n) - (b mod n)) / n) by nia. + nia. +Qed. +Example Zplus_mod: forall a b n : Z, (a + b) mod n = (a mod n + b mod n) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a + b) / n = (a / n) + (b / n) + ((a mod n) + (b mod n)) / n) by nia. + nia. +Qed. +Example Zmult_mod: forall a b n : Z, (a * b) mod n = (a mod n * (b mod n)) mod n. +Proof. + intros a b n. + destruct (Z_zerop n); [ subst; nia | ]. + assert ((a * b) / n = n * (a / n) * (b / n) + (a mod n) * (b / n) + (a / n) * (b mod n) + ((a mod n) * (b mod n)) / n) + by nia. + nia. +Qed. +Example Z_mod_mod: forall a n : Z, n <> 0 -> (a mod n) mod n = a mod n. Proof. t. Qed. +Example Z_mod_div: forall a b : Z, b <> 0 -> a mod b / b = 0. Proof. intros; nia. Qed. +Example Z_div_exact_full_1: forall a b : Z, a = b * (a / b) -> a mod b = 0. Proof. intros; nia. Qed. +Example Z_mod_pos_bound: forall a b : Z, 0 < b -> 0 <= a mod b < b. Proof. intros; nia. Qed. +Example Z_mod_sign_mul: forall a b : Z, b <> 0 -> 0 <= a mod b * b. Proof. intros; nia. Qed. +Example Z_mod_neg_bound: forall a b : Z, b < 0 -> b < a mod b <= 0. Proof. intros; nia. Qed. +Example Z_mod_neg: forall a b : Z, b < 0 -> b < a mod b <= 0. Proof. intros; nia. Qed. +Example div_mod_small: forall x y : Z, 0 <= x < y -> x mod y = x. Proof. t. Qed. +Example Zmod_small: forall a n : Z, 0 <= a < n -> a mod n = a. Proof. t. Qed. +Example Z_mod_small: forall a b : Z, 0 <= a < b -> a mod b = a. Proof. t. Qed. +Example Z_div_zero_opp_full: forall a b : Z, a mod b = 0 -> - a / b = - (a / b). Proof. intros; nia. Qed. +Example Z_mod_zero_opp: forall a b : Z, b > 0 -> a mod b = 0 -> - a mod b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or (a/b) (-(-a/b))). + nia. +Qed. +Example Z_div_zero_opp_r: forall a b : Z, a mod b = 0 -> a / - b = - (a / b). Proof. intros; nia. Qed. +Example Z_mod_lt: forall a b : Z, b > 0 -> 0 <= a mod b < b. Proof. intros; nia. Qed. +Example Z_mod_opp_opp: forall a b : Z, b <> 0 -> - a mod - b = - (a mod b). +Proof. + intros a b. + pose proof (Z_eq_dec_or ((-a)/(-b)) ((a/b))). + nia. +Qed. +Example Z_mod_bound_pos: forall a b : Z, 0 <= a -> 0 < b -> 0 <= a mod b < b. Proof. intros; nia. Qed. +Example Z_mod_opp_l_z: forall a b : Z, b <> 0 -> a mod b = 0 -> - a mod b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or (a/b) (-(-a/b))). + nia. +Qed. +Example Z_mod_plus: forall a b c : Z, c > 0 -> (a + b * c) mod c = a mod c. +Proof. + intros a b c. + pose proof (Z_eq_dec_or ((a+b*c)/c) (a/c+b)). + nia. +Qed. +Example Z_mod_opp_r_z: forall a b : Z, b <> 0 -> a mod b = 0 -> a mod - b = 0. +Proof. + intros a b. + pose proof (Z_eq_dec_or (a/b) (-(a/-b))). + nia. +Qed. +Example Zmod_eq: forall a b : Z, b > 0 -> a mod b = a - a / b * b. Proof. intros; nia. Qed. +Example Z_div_exact_2: forall a b : Z, b > 0 -> a mod b = 0 -> a = b * (a / b). Proof. intros; nia. Qed. +Example Z_div_mod_eq: forall a b : Z, b > 0 -> a = b * (a / b) + a mod b. Proof. intros; nia. Qed. +Example Z_div_exact_1: forall a b : Z, b > 0 -> a = b * (a / b) -> a mod b = 0. Proof. intros; nia. Qed. +Example Z_mod_add: forall a b c : Z, c <> 0 -> (a + b * c) mod c = a mod c. +Proof. + intros a b c. + pose proof (Z_eq_dec_or ((a+b*c)/c) (a/c+b)). + nia. +Qed. +Example Z_mod_nz_opp_r: forall a b : Z, a mod b <> 0 -> a mod - b = a mod b - b. +Proof. + intros a b. + assert (a mod b <> 0 -> a / -b = -(a/b)-1) by t. + nia. +Qed. +Example Z_mul_mod_idemp_l: forall a b n : Z, n <> 0 -> (a mod n * b) mod n = (a * b) mod n. +Proof. + intros a b n ?. + assert (((a mod n) * b) / n = (b / n) * (a mod n) + ((b mod n) * (a mod n)) / n) + by nia. + assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((b mod n) * (a mod n)) / n) + by nia. + nia. +Qed. +Example Z_mod_nz_opp_full: forall a b : Z, a mod b <> 0 -> - a mod b = b - a mod b. +Proof. + intros a b. + assert (a mod b <> 0 -> -a/b = -1-a/b) by nia. + nia. +Qed. +Example Z_add_mod_idemp_r: forall a b n : Z, n <> 0 -> (a + b mod n) mod n = (a + b) mod n. +Proof. + intros a b n ?. + assert ((a + b mod n) / n = (a / n) + (a mod n + b mod n) / n) by nia. + assert ((a + b) / n = (a / n) + (b / n) + (a mod n + b mod n) / n) by nia. + nia. +Qed. +Example Z_add_mod_idemp_l: forall a b n : Z, n <> 0 -> (a mod n + b) mod n = (a + b) mod n. +Proof. + intros a b n ?. + assert ((a mod n + b) / n = (b / n) + (a mod n + b mod n) / n) by nia. + assert ((a + b) / n = (a / n) + (b / n) + (a mod n + b mod n) / n) by nia. + nia. +Qed. +Example Z_mul_mod_idemp_r: forall a b n : Z, n <> 0 -> (a * (b mod n)) mod n = (a * b) mod n. +Proof. + intros a b n ?. + assert ((a * (b mod n)) / n = (a / n) * (b mod n) + ((a mod n) * (b mod n)) / n) + by nia. + assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((a mod n) * (b mod n)) / n) + by nia. + nia. +Qed. +Example Zmod_eq_full: forall a b : Z, b <> 0 -> a mod b = a - a / b * b. Proof. intros; nia. Qed. +Example div_eq: forall x y : Z, y <> 0 -> x mod y = 0 -> x / y * y = x. Proof. intros; nia. Qed. +Example Z_mod_eq: forall a b : Z, b <> 0 -> a mod b = a - b * (a / b). Proof. intros; nia. Qed. +Example Z_mod_sign_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> Z.sgn (a mod b) = Z.sgn b. Proof. intros; nia. Qed. +Example Z_div_exact_full_2: forall a b : Z, b <> 0 -> a mod b = 0 -> a = b * (a / b). Proof. intros; nia. Qed. +Example Z_div_mod: forall a b : Z, b <> 0 -> a = b * (a / b) + a mod b. Proof. intros; nia. Qed. +Example Z_add_mod: forall a b n : Z, n <> 0 -> (a + b) mod n = (a mod n + b mod n) mod n. +Proof. + intros a b n ?. + assert ((a + b) / n = (a / n) + (b / n) + (a mod n + b mod n) / n) by nia. + nia. +Qed. +Example Z_mul_mod: forall a b n : Z, n <> 0 -> (a * b) mod n = (a mod n * (b mod n)) mod n. +Proof. + intros a b n ?. + assert ((a * b) / n = (b / n) * (a / n) * n + (b / n) * (a mod n) + (b mod n) * (a / n) + ((a mod n) * (b mod n)) / n) + by nia. + nia. +Qed. +Example Z_div_exact: forall a b : Z, b <> 0 -> a = b * (a / b) <-> a mod b = 0. Proof. intros; nia. Qed. +Example Z_div_opp_l_z: forall a b : Z, b <> 0 -> a mod b = 0 -> - a / b = - (a / b). Proof. intros; nia. Qed. +Example Z_div_opp_r_z: forall a b : Z, b <> 0 -> a mod b = 0 -> a / - b = - (a / b). Proof. intros; nia. Qed. +Example Z_mod_opp_r_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> a mod - b = a mod b - b. +Proof. + intros a b. + assert (a mod b <> 0 -> a/(-b) = -1-a/b) by nia. + nia. +Qed. +Example Z_mul_mod_distr_r: forall a b c : Z, b <> 0 -> c <> 0 -> (a * c) mod (b * c) = a mod b * c. +Proof. + intros a b c. + pose proof (Z_eq_dec_or ((a*c)/(b*c)) (a/b)). + nia. +Qed. +Example Z_mul_mod_distr_l: forall a b c : Z, b <> 0 -> c <> 0 -> (c * a) mod (c * b) = c * (a mod b). +Proof. + intros a b c. + pose proof (Z_eq_dec_or ((c*a)/(c*b)) (a/b)). + nia. +Qed. +Example Z_mod_opp_l_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> - a mod b = b - a mod b. +Proof. + intros a b. + assert (a mod b <> 0 -> -a/b = -1-a/b) by nia. + nia. +Qed. +Example mod_eq: forall x x' y : Z, x / y = x' / y -> x mod y = x' mod y -> y <> 0 -> x = x'. Proof. intros; nia. Qed. +Example Z_div_nz_opp_r: forall a b : Z, a mod b <> 0 -> a / - b = - (a / b) - 1. Proof. intros; nia. Qed. +Example Z_div_nz_opp_full: forall a b : Z, a mod b <> 0 -> - a / b = - (a / b) - 1. Proof. intros; nia. Qed. +Example Zmod_unique: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> r = a mod b. +Proof. + intros a b q r ??. + assert (q = a / b) by nia. + nia. +Qed. +Example Z_mod_unique_neg: forall a b q r : Z, b < r <= 0 -> a = b * q + r -> r = a mod b. +Proof. + intros a b q r ??. + assert (q = a / b) by nia. + nia. +Qed. +Example Z_mod_unique_pos: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> r = a mod b. +Proof. + intros a b q r ??. + assert (q = a / b) by nia. + nia. +Qed. +Example Z_rem_mul_r: forall a b c : Z, b <> 0 -> 0 < c -> a mod (b * c) = a mod b + b * ((a / b) mod c). +Proof. + intros a b c ??. + assert (a / (b * c) = ((a / b) / c)) by nia. + nia. +Qed. +Example Z_mod_bound_or: forall a b : Z, b <> 0 -> 0 <= a mod b < b \/ b < a mod b <= 0. Proof. intros; nia. Qed. +Example Z_div_opp_l_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> - a / b = - (a / b) - 1. Proof. intros; nia. Qed. +Example Z_div_opp_r_nz: forall a b : Z, b <> 0 -> a mod b <> 0 -> a / - b = - (a / b) - 1. Proof. intros; nia. Qed. +Example Z_mod_small_iff: forall a b : Z, b <> 0 -> a mod b = a <-> 0 <= a < b \/ b < a <= 0. Proof. t. Qed. +Example Z_mod_unique: forall a b q r : Z, 0 <= r < b \/ b < r <= 0 -> a = b * q + r -> r = a mod b. +Proof. + intros a b q r ??. + assert (q = a/b) by nia. + nia. +Qed. +Example Z_opp_mod_bound_or: forall a b : Z, b <> 0 -> 0 <= - (a mod b) < - b \/ - b < - (a mod b) <= 0. Proof. intros; nia. Qed. + +Example Zdiv_0_r: forall a : Z, a / 0 = 0. Proof. intros; nia. Qed. +Example Zdiv_0_l: forall a : Z, 0 / a = 0. Proof. intros; nia. Qed. +Example Z_div_1_r: forall a : Z, a / 1 = a. Proof. intros; nia. Qed. +Example Zdiv_1_r: forall a : Z, a / 1 = a. Proof. intros; nia. Qed. +Example Zdiv_opp_opp: forall a b : Z, - a / - b = a / b. Proof. intros; nia. Qed. +Example Z_div_0_l: forall a : Z, a <> 0 -> 0 / a = 0. Proof. intros; nia. Qed. +Example Z_div_pos: forall a b : Z, b > 0 -> 0 <= a -> 0 <= a / b. Proof. intros; nia. Qed. +Example Z_div_ge0: forall a b : Z, b > 0 -> a >= 0 -> a / b >= 0. Proof. intros; nia. Qed. +Example Z_div_pos': forall a b : Z, 0 <= a -> 0 < b -> 0 <= a / b. Proof. intros; nia. Qed. +Example Z_mult_div_ge: forall a b : Z, b > 0 -> b * (a / b) <= a. Proof. intros; nia. Qed. +Example Z_mult_div_ge_neg: forall a b : Z, b < 0 -> b * (a / b) >= a. Proof. intros; nia. Qed. +Example Z_mul_div_le: forall a b : Z, 0 < b -> b * (a / b) <= a. Proof. intros; nia. Qed. +Example Z_mul_div_ge: forall a b : Z, b < 0 -> a <= b * (a / b). Proof. intros; nia. Qed. +Example Z_div_same: forall a : Z, a > 0 -> a / a = 1. Proof. intros; nia. Qed. +Example Z_div_mult: forall a b : Z, b > 0 -> a * b / b = a. Proof. intros; nia. Qed. +Example Z_mul_succ_div_gt: forall a b : Z, 0 < b -> a < b * Z.succ (a / b). Proof. intros; nia. Qed. +Example Z_mul_succ_div_lt: forall a b : Z, b < 0 -> b * Z.succ (a / b) < a. Proof. intros; nia. Qed. +Example Zdiv_1_l: forall a : Z, 1 < a -> 1 / a = 0. Proof. intros; nia. Qed. +Example Z_div_1_l: forall a : Z, 1 < a -> 1 / a = 0. Proof. intros; nia. Qed. +Example Z_div_str_pos: forall a b : Z, 0 < b <= a -> 0 < a / b. Proof. intros; nia. Qed. +Example Z_div_ge: forall a b c : Z, c > 0 -> a >= b -> a / c >= b / c. Proof. intros; nia. Qed. +Example Z_div_mult_full: forall a b : Z, b <> 0 -> a * b / b = a. Proof. intros; nia. Qed. +Example Z_div_same': forall a : Z, a <> 0 -> a / a = 1. Proof. intros; nia. Qed. +Example Zdiv_lt_upper_bound: forall a b q : Z, 0 < b -> a < q * b -> a / b < q. Proof. intros; nia. Qed. +Example Z_div_mul: forall a b : Z, b <> 0 -> a * b / b = a. Proof. intros; nia. Qed. +Example Z_div_lt: forall a b : Z, 0 < a -> 1 < b -> a / b < a. Proof. intros; nia. Qed. +Example Z_div_le_mono: forall a b c : Z, 0 < c -> a <= b -> a / c <= b / c. Proof. intros; nia. Qed. +Example Zdiv_sgn: forall a b : Z, 0 <= Z.sgn (a / b) * Z.sgn a * Z.sgn b. Proof. intros; nia. Qed. +Example Z_div_same_full: forall a : Z, a <> 0 -> a / a = 1. Proof. intros; nia. Qed. +Example Z_div_lt_upper_bound: forall a b q : Z, 0 < b -> a < b * q -> a / b < q. Proof. intros; nia. Qed. +Example Z_div_le: forall a b c : Z, c > 0 -> a <= b -> a / c <= b / c. Proof. intros; nia. Qed. +Example Z_div_le_lower_bound: forall a b q : Z, 0 < b -> b * q <= a -> q <= a / b. Proof. intros; nia. Qed. +Example Zdiv_le_lower_bound: forall a b q : Z, 0 < b -> q * b <= a -> q <= a / b. Proof. intros; nia. Qed. +Example Zdiv_le_upper_bound: forall a b q : Z, 0 < b -> a <= q * b -> a / b <= q. Proof. intros; nia. Qed. +Example Z_div_le_upper_bound: forall a b q : Z, 0 < b -> a <= b * q -> a / b <= q. Proof. intros; nia. Qed. +Example Z_div_small: forall a b : Z, 0 <= a < b -> a / b = 0. Proof. intros; nia. Qed. +Example Zdiv_small: forall a b : Z, 0 <= a < b -> a / b = 0. Proof. intros; nia. Qed. +Example Z_div_opp_opp: forall a b : Z, b <> 0 -> - a / - b = a / b. Proof. intros; nia. Qed. +Example Zdiv_mult_cancel_r: forall a b c : Z, c <> 0 -> a * c / (b * c) = a / b. Proof. intros; nia. Qed. +Example Z_div_unique_exact: forall a b q : Z, b <> 0 -> a = b * q -> q = a / b. Proof. intros; nia. Qed. +Example Zdiv_mult_cancel_l: forall a b c : Z, c <> 0 -> c * a / (c * b) = a / b. Proof. intros; nia. Qed. +Example Zdiv_le_compat_l: forall p q r : Z, 0 <= p -> 0 < q < r -> p / r <= p / q. +Proof. + intros p q r ??. + assert (p mod r <= p mod q \/ p mod q <= p mod r) by nia. + assert (0 <= p / r) by nia. + assert (0 <= p / q) by nia. + nia. +Qed. +Example Z_div_le_compat_l: forall p q r : Z, 0 <= p -> 0 < q <= r -> p / r <= p / q. +Proof. + intros p q r ??. + assert (p mod r <= p mod q \/ p mod q <= p mod r) by nia. + assert (0 <= p / r) by nia. + assert (0 <= p / q) by nia. + nia. +Qed. +Example Zdiv_Zdiv: forall a b c : Z, 0 <= b -> 0 <= c -> a / b / c = a / (b * c). Proof. intros; nia. Qed. +Example Z_div_plus: forall a b c : Z, c > 0 -> (a + b * c) / c = a / c + b. Proof. intros; nia. Qed. +Example Z_div_lt': forall a b : Z, b >= 2 -> a > 0 -> a / b < a. Proof. intros; nia. Qed. +Example Zdiv_mult_le: forall a b c : Z, 0 <= a -> 0 <= b -> 0 <= c -> c * (a / b) <= c * a / b. Proof. intros; nia. Qed. +Example Z_div_add_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b. Proof. intros; nia. Qed. +Example Z_div_plus_full_l: forall a b c : Z, b <> 0 -> (a * b + c) / b = a + c / b. Proof. intros; nia. Qed. +Example Z_div_add: forall a b c : Z, c <> 0 -> (a + b * c) / c = a / c + b. Proof. intros; nia. Qed. +Example Z_div_plus_full: forall a b c : Z, c <> 0 -> (a + b * c) / c = a / c + b. Proof. intros; nia. Qed. +Example Z_div_mul_le: forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b. Proof. intros; nia. Qed. +Example Z_div_mul_cancel_r: forall a b c : Z, b <> 0 -> c <> 0 -> a * c / (b * c) = a / b. Proof. intros; nia. Qed. +Example Z_div_div: forall a b c : Z, b <> 0 -> 0 < c -> a / b / c = a / (b * c). Proof. intros; nia. Qed. +Example Z_div_mul_cancel_l: forall a b c : Z, b <> 0 -> c <> 0 -> c * a / (c * b) = a / b. Proof. intros; nia. Qed. +Example Z_div_unique_neg: forall a b q r : Z, b < r <= 0 -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed. +Example Zdiv_unique: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed. +Example Z_div_unique_pos: forall a b q r : Z, 0 <= r < b -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed. +Example Z_div_small_iff: forall a b : Z, b <> 0 -> a / b = 0 <-> 0 <= a < b \/ b < a <= 0. Proof. intros; nia. Qed. +Example Z_div_unique: forall a b q r : Z, 0 <= r < b \/ b < r <= 0 -> a = b * q + r -> q = a / b. Proof. intros; nia. Qed. + +(** Now we do the same, but with [Z.quot] and [Z.rem] instead. *) +Lemma N2Z_inj_quot : forall n m : N, Z.of_N (n / m) = Z.of_N n ÷ Z.of_N m. Proof. intros; nia. Qed. +Lemma N2Z_inj_rem : forall n m : N, Z.of_N (n mod m) = Z.rem (Z.of_N n) (Z.of_N m). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0. +Proof. intros; destruct (Z_zerop (a ÷ b)); nia. Qed. +Lemma OrdersEx_Z_as_DT_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros; destruct (Z_zerop (a ÷ b)); nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c). +Proof. intros; assert (0 < b * c) by nia; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. +Proof. + intros. + destruct (Z_zerop p), (Z_zerop (p ÷ r)), (Z_zerop (p ÷ q)); subst; [ nia.. | ]. + assert (0 < q) by nia; assert (0 < r) by nia; assert (0 < p) by nia. + nia. +Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. +Proof. + intros. + destruct (Z_zerop p), (Z_zerop (p ÷ r)), (Z_zerop (p ÷ q)); [ subst; nia.. | ]. + assert (0 < p) by nia; assert (0 < r) by nia. + nia. +Qed. +Lemma OrdersEx_Z_as_DT_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c. +Proof. + intros. + destruct (Z_zerop a), (Z_zerop b), (Z_zerop (a ÷ c)), (Z_zerop (b ÷ c)); [ subst; nia.. | ]. + nia. +Qed. +Lemma OrdersEx_Z_as_DT_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b. +Proof. + intros. + assert (c * b <> 0) by nia. + destruct (Z_zerop a), (Z_zerop (c * a)); subst; [ nia | exfalso; nia.. | ]. +Abort. +Lemma OrdersEx_Z_as_DT_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. Abort. +Lemma OrdersEx_Z_as_DT_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; assert (b * c <> 0) by nia. Abort. +Lemma OrdersEx_Z_as_DT_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_DT_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0. Proof. intros. Fail nia. Abort. +Lemma OrdersEx_Z_as_OT_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros. Fail nia. Abort. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros. Abort. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros. Fail nia. Abort. +Lemma OrdersEx_Z_as_OT_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros. Fail nia. Abort. +Lemma OrdersEx_Z_as_OT_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros. Abort. +Lemma OrdersEx_Z_as_OT_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros. Abort. +Lemma OrdersEx_Z_as_OT_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros. Abort. +Lemma OrdersEx_Z_as_OT_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma OrdersEx_Z_as_OT_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma Z2N_inj_quot : forall n m : Z, 0 <= n -> 0 <= m -> Z.to_N (n ÷ m) = (Z.to_N n / Z.to_N m)%N. +Proof. intros; destruct (Z_zerop n), (Z_zerop m), (Z_zerop (n ÷ m)); [ subst; try nia.. | ]. Abort. +Lemma Z2N_inj_rem : forall n m : Z, 0 <= n -> 0 <= m -> Z.to_N (Z.rem n m) = (Z.to_N n mod Z.to_N m)%N. Proof. intros. Abort. +Lemma Zabs2N_inj_quot : forall n m : Z, Z.abs_N (n ÷ m) = (Z.abs_N n / Z.abs_N m)%N. Proof. intros. Abort. +Lemma Zabs2N_inj_rem : forall n m : Z, Z.abs_N (Z.rem n m) = (Z.abs_N n mod Z.abs_N m)%N. Proof. intros. Abort. +(* Some of these don't work, and I haven't gone through and figured out which ones yet, so they're all commented out for now *) +(* +Lemma Z_add_rem : forall a b n : Z, n <> 0 -> 0 <= a * b -> Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Z_add_rem_idemp_l : forall a b n : Z, n <> 0 -> 0 <= a * b -> Z.rem (Z.rem a n + b) n = Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma Z_add_rem_idemp_r : forall a b n : Z, n <> 0 -> 0 <= a * b -> Z.rem (a + Z.rem b n) n = Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_add_rem : forall a b n : Z, n <> 0 -> 0 <= a * b -> ZBinary.Z.rem (a + b) n = ZBinary.Z.rem (ZBinary.Z.rem a n + ZBinary.Z.rem b n) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_add_rem_idemp_l : forall a b n : Z, n <> 0 -> 0 <= a * b -> ZBinary.Z.rem (ZBinary.Z.rem a n + b) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_add_rem_idemp_r : forall a b n : Z, n <> 0 -> 0 <= a * b -> ZBinary.Z.rem (a + ZBinary.Z.rem b n) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_gcd_quot_gcd : forall a b g : Z, g <> 0 -> g = ZBinary.Z.gcd a b -> ZBinary.Z.gcd (a ÷ g) (b ÷ g) = 1. Proof. intros; nia. Qed. +Lemma ZBinary_Z_gcd_rem : forall a b : Z, b <> 0 -> ZBinary.Z.gcd (ZBinary.Z.rem a b) b = ZBinary.Z.gcd b a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mod_mul_r : forall a b c : Z, b <> 0 -> c <> 0 -> ZBinary.Z.rem a (b * c) = ZBinary.Z.rem a b + b * ZBinary.Z.rem (a ÷ b) c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_pred_quot_gt : forall a b : Z, 0 <= a -> b < 0 -> a < b * ZBinary.Z.pred (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_pred_quot_lt : forall a b : Z, a <= 0 -> 0 < b -> b * ZBinary.Z.pred (a ÷ b) < a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_rem_distr_l : forall a b c : Z, b <> 0 -> c <> 0 -> ZBinary.Z.rem (c * a) (c * b) = c * ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_rem_distr_r : forall a b c : Z, b <> 0 -> c <> 0 -> ZBinary.Z.rem (a * c) (b * c) = ZBinary.Z.rem a b * c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_rem : forall a b n : Z, n <> 0 -> ZBinary.Z.rem (a * b) n = ZBinary.Z.rem (ZBinary.Z.rem a n * ZBinary.Z.rem b n) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_rem_idemp_l : forall a b n : Z, n <> 0 -> ZBinary.Z.rem (ZBinary.Z.rem a n * b) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_rem_idemp_r : forall a b n : Z, n <> 0 -> ZBinary.Z.rem (a * ZBinary.Z.rem b n) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_succ_quot_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * ZBinary.Z.succ (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_mul_succ_quot_lt : forall a b : Z, a <= 0 -> b < 0 -> b * ZBinary.Z.succ (a ÷ b) < a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_add_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a + b) n = ZBinary.Z.rem (ZBinary.Z.rem a n + ZBinary.Z.rem b n) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_add_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (ZBinary.Z.rem a n + b) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_add_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a + ZBinary.Z.rem b n) n = ZBinary.Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_exact : forall a b : Z, 0 <= a -> 0 < b -> a = b * (a ÷ b) <-> ZBinary.Z.rem a b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_0_l : forall a : Z, 0 < a -> ZBinary.Z.rem 0 a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_1_l : forall a : Z, 1 < a -> ZBinary.Z.rem 1 a = 1. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_1_r : forall a : Z, 0 <= a -> ZBinary.Z.rem a 1 = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> ZBinary.Z.rem (a + b * c) c = ZBinary.Z.rem a c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_divides : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b = 0 <-> (exists c : Z, a = b * c). Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_le : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b <= a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_mod : forall a n : Z, 0 <= a -> 0 < n -> ZBinary.Z.rem (ZBinary.Z.rem a n) n = ZBinary.Z.rem a n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_mul : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem (a * b) b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_mul_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> ZBinary.Z.rem a (b * c) = ZBinary.Z.rem a b + b * ZBinary.Z.rem (a ÷ b) c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_same : forall a : Z, 0 < a -> ZBinary.Z.rem a a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_small : forall a b : Z, 0 <= a < b -> ZBinary.Z.rem a b = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_small_iff : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b = a <-> a < b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mod_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_distr_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> ZBinary.Z.rem (c * a) (c * b) = c * ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_distr_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> ZBinary.Z.rem (a * c) (b * c) = ZBinary.Z.rem a b * c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a * b) n = ZBinary.Z.rem (ZBinary.Z.rem a n * ZBinary.Z.rem b n) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (ZBinary.Z.rem a n * b) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> ZBinary.Z.rem (a * ZBinary.Z.rem b n) n = ZBinary.Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_NZQuot_mul_succ_div_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * ZBinary.Z.succ (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_Private_Div_Quot2Div_div_mod : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + ZBinary.Z.rem a b. Proof. intros; nia. Qed. +ZBinary_Z_Private_Div_Quot2Div_div_wd Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) ZBinary.Z.quot +Lemma ZBinary_Z_Private_Div_Quot2Div_mod_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= ZBinary.Z.rem a b < b. Proof. intros; nia. Qed. +ZBinary_Z_Private_Div_Quot2Div_mod_wd Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) ZBinary.Z.rem +Lemma ZBinary_Z_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_abs : forall a b : Z, b <> 0 -> ZBinary.Z.abs a ÷ ZBinary.Z.abs b = ZBinary.Z.abs (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_abs_l : forall a b : Z, b <> 0 -> ZBinary.Z.abs a ÷ b = ZBinary.Z.sgn a * (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_abs_r : forall a b : Z, b <> 0 -> a ÷ ZBinary.Z.abs b = ZBinary.Z.sgn b * (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_div : forall a b : Z, b <> 0 -> a ÷ b = ZBinary.Z.sgn a * ZBinary.Z.sgn b * (ZBinary.Z.abs a / ZBinary.Z.abs b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_exact : forall a b : Z, b <> 0 -> a = b * (a ÷ b) <-> ZBinary.Z.rem a b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_rem' : forall a b : Z, a = b * (a ÷ b) + ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_rem : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_small_iff : forall a b : Z, b <> 0 -> a ÷ b = 0 <-> ZBinary.Z.abs a < ZBinary.Z.abs b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +ZBinary_Z_quot_wd Morphisms.Proper (Morphisms.respectful ZBinary.Z.eq (Morphisms.respectful ZBinary.Z.eq ZBinary.Z.eq)) ZBinary.Z.quot +Lemma ZBinary_Z_rem_0_l : forall a : Z, a <> 0 -> ZBinary.Z.rem 0 a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_1_l : forall a : Z, 1 < a -> ZBinary.Z.rem 1 a = 1. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_1_r : forall a : Z, ZBinary.Z.rem a 1 = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_abs : forall a b : Z, b <> 0 -> ZBinary.Z.rem (ZBinary.Z.abs a) (ZBinary.Z.abs b) = ZBinary.Z.abs (ZBinary.Z.rem a b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_abs_l : forall a b : Z, b <> 0 -> ZBinary.Z.rem (ZBinary.Z.abs a) b = ZBinary.Z.abs (ZBinary.Z.rem a b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_abs_r : forall a b : Z, b <> 0 -> ZBinary.Z.rem a (ZBinary.Z.abs b) = ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> ZBinary.Z.rem (a + b * c) c = ZBinary.Z.rem a c. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_bound_abs : forall a b : Z, b <> 0 -> ZBinary.Z.abs (ZBinary.Z.rem a b) < ZBinary.Z.abs b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= ZBinary.Z.rem a b < b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_eq : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = a - b * (a ÷ b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_le : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b <= a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_mod_eq_0 : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = 0 <-> a mod b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_mod : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = ZBinary.Z.sgn a * (ZBinary.Z.abs a mod ZBinary.Z.abs b). Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_mod_nonneg : forall a b : Z, 0 <= a -> 0 < b -> ZBinary.Z.rem a b = a mod b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_mul : forall a b : Z, b <> 0 -> ZBinary.Z.rem (a * b) b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_nonneg : forall a b : Z, b <> 0 -> 0 <= a -> 0 <= ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_nonpos : forall a b : Z, b <> 0 -> a <= 0 -> ZBinary.Z.rem a b <= 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_opp_l : forall a b : Z, b <> 0 -> ZBinary.Z.rem (- a) b = - ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_opp_l' : forall a b : Z, ZBinary.Z.rem (- a) b = - ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_opp_opp : forall a b : Z, b <> 0 -> ZBinary.Z.rem (- a) (- b) = - ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_opp_r : forall a b : Z, b <> 0 -> ZBinary.Z.rem a (- b) = ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_opp_r' : forall a b : Z, ZBinary.Z.rem a (- b) = ZBinary.Z.rem a b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_quot : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b ÷ b = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_rem : forall a n : Z, n <> 0 -> ZBinary.Z.rem (ZBinary.Z.rem a n) n = ZBinary.Z.rem a n. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_same : forall a : Z, a <> 0 -> ZBinary.Z.rem a a = 0. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_sign : forall a b : Z, a <> 0 -> b <> 0 -> ZBinary.Z.sgn (ZBinary.Z.rem a b) <> - ZBinary.Z.sgn a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_sign_mul : forall a b : Z, b <> 0 -> 0 <= ZBinary.Z.rem a b * a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_sign_nz : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b <> 0 -> ZBinary.Z.sgn (ZBinary.Z.rem a b) = ZBinary.Z.sgn a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_small : forall a b : Z, 0 <= a < b -> ZBinary.Z.rem a b = a. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_small_iff : forall a b : Z, b <> 0 -> ZBinary.Z.rem a b = a <-> ZBinary.Z.abs a < ZBinary.Z.abs b. Proof. intros; nia. Qed. +Lemma ZBinary_Z_rem_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = ZBinary.Z.rem a b. Proof. intros; nia. Qed. +ZBinary_Z_rem_wd Morphisms.Proper (Morphisms.respectful ZBinary.Z.eq (Morphisms.respectful ZBinary.Z.eq ZBinary.Z.eq)) ZBinary.Z.rem +Lemma Z_gcd_quot_gcd : forall a b g : Z, g <> 0 -> g = Z.gcd a b -> Z.gcd (a ÷ g) (b ÷ g) = 1. Proof. intros; nia. Qed. +Lemma Z_gcd_rem : forall a b : Z, b <> 0 -> Z.gcd (Z.rem a b) b = Z.gcd b a. Proof. intros; nia. Qed. +Lemma Z_mod_mul_r : forall a b c : Z, b <> 0 -> c <> 0 -> Z.rem a (b * c) = Z.rem a b + b * Z.rem (a ÷ b) c. Proof. intros; nia. Qed. +Lemma Z_mul_pred_quot_gt : forall a b : Z, 0 <= a -> b < 0 -> a < b * Z.pred (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_mul_pred_quot_lt : forall a b : Z, a <= 0 -> 0 < b -> b * Z.pred (a ÷ b) < a. Proof. intros; nia. Qed. +Lemma Z_mul_quot_ge : forall a b : Z, a <= 0 -> b <> 0 -> a <= b * (a ÷ b) <= 0. Proof. intros; nia. Qed. +Lemma Z_mul_quot_le : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma Z_mul_rem_distr_l : forall a b c : Z, b <> 0 -> c <> 0 -> Z.rem (c * a) (c * b) = c * Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_mul_rem_distr_r : forall a b c : Z, b <> 0 -> c <> 0 -> Z.rem (a * c) (b * c) = Z.rem a b * c. Proof. intros; nia. Qed. +Lemma Z_mul_rem : forall a b n : Z, n <> 0 -> Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Z_mul_rem_idemp_l : forall a b n : Z, n <> 0 -> Z.rem (Z.rem a n * b) n = Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma Z_mul_rem_idemp_r : forall a b n : Z, n <> 0 -> Z.rem (a * Z.rem b n) n = Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma Z_mul_succ_quot_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * Z.succ (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_mul_succ_quot_lt : forall a b : Z, a <= 0 -> b < 0 -> b * Z.succ (a ÷ b) < a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_add_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_add_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (Z.rem a n + b) n = Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_add_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a + Z.rem b n) n = Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_0_l : forall a : Z, 0 < a -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_1_r : forall a : Z, 0 <= a -> a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_add_l : forall a b c : Z, 0 <= c -> 0 <= a * b + c -> 0 < b -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_div : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_exact : forall a b : Z, 0 <= a -> 0 < b -> a = b * (a ÷ b) <-> Z.rem a b = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_le_lower_bound : forall a b q : Z, 0 <= a -> 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_le_mono : forall a b c : Z, 0 < c -> 0 <= a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_le_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_mul_cancel_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_mul_cancel_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_mul : forall a b : Z, 0 <= a -> 0 < b -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_same : forall a : Z, 0 < a -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_small_iff : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = 0 <-> a < b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_str_pos_iff : forall a b : Z, 0 <= a -> 0 < b -> 0 < a ÷ b <-> b <= a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_unique_exact : forall a b q : Z, 0 <= a -> 0 < b -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_div_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_0_l : forall a : Z, 0 < a -> Z.rem 0 a = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_1_l : forall a : Z, 1 < a -> Z.rem 1 a = 1. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_1_r : forall a : Z, 0 <= a -> Z.rem a 1 = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_add : forall a b c : Z, 0 <= a -> 0 <= a + b * c -> 0 < c -> Z.rem (a + b * c) c = Z.rem a c. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_divides : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = 0 <-> (exists c : Z, a = b * c). Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_le : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b <= a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_mod : forall a n : Z, 0 <= a -> 0 < n -> Z.rem (Z.rem a n) n = Z.rem a n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_mul : forall a b : Z, 0 <= a -> 0 < b -> Z.rem (a * b) b = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_mul_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> Z.rem a (b * c) = Z.rem a b + b * Z.rem (a ÷ b) c. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_same : forall a : Z, 0 < a -> Z.rem a a = 0. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_small : forall a b : Z, 0 <= a < b -> Z.rem a b = a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_small_iff : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = a <-> a < b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mod_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_div_le : forall a b : Z, 0 <= a -> 0 < b -> b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_mod_distr_l : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> Z.rem (c * a) (c * b) = c * Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_mod_distr_r : forall a b c : Z, 0 <= a -> 0 < b -> 0 < c -> Z.rem (a * c) (b * c) = Z.rem a b * c. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_mod : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_mod_idemp_l : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (Z.rem a n * b) n = Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_mod_idemp_r : forall a b n : Z, 0 <= a -> 0 <= b -> 0 < n -> Z.rem (a * Z.rem b n) n = Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma Z_Private_Div_NZQuot_mul_succ_div_gt : forall a b : Z, 0 <= a -> 0 < b -> a < b * Z.succ (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_Private_Div_Quot2Div_div_mod : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + Z.rem a b. Proof. intros; nia. Qed. +Z_Private_Div_Quot2Div_div_wd Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) Z.quot +Lemma Z_Private_Div_Quot2Div_mod_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= Z.rem a b < b. Proof. intros; nia. Qed. +Z_Private_Div_Quot2Div_mod_wd Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq)) Z.rem +Lemma Z_quot_0_l : forall a : Z, a <> 0 -> 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma Z_quot_0_r_ext : forall x y : Z, y = 0 -> x ÷ y = 0. Proof. intros; nia. Qed. +Lemma Z_quot_1_l : forall a : Z, 1 < a -> 1 ÷ a = 0. Proof. intros; nia. Qed. +Lemma Z_quot_1_r : forall a : Z, a ÷ 1 = a. Proof. intros; nia. Qed. +Lemma Zquot2_quot : forall n : Z, Z.quot2 n = n ÷ 2. Proof. intros; nia. Qed. +Lemma Z_quot_abs : forall a b : Z, b <> 0 -> Z.abs a ÷ Z.abs b = Z.abs (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_quot_abs_l : forall a b : Z, b <> 0 -> Z.abs a ÷ b = Z.sgn a * (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_quot_abs_r : forall a b : Z, b <> 0 -> a ÷ Z.abs b = Z.sgn b * (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_quot_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma Z_quot_add_l : forall a b c : Z, b <> 0 -> 0 <= (a * b + c) * c -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_div : forall a b : Z, b <> 0 -> a ÷ b = Z.sgn a * Z.sgn b * (Z.abs a / Z.abs b). Proof. intros; nia. Qed. +Lemma Z_quot_div_nonneg : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b. Proof. intros; nia. Qed. +Lemma Z_quot_exact : forall a b : Z, b <> 0 -> a = b * (a ÷ b) <-> Z.rem a b = 0. Proof. intros; nia. Qed. +Lemma Z_quot_le_compat_l : forall p q r : Z, 0 <= p -> 0 < q <= r -> p ÷ r <= p ÷ q. Proof. intros; nia. Qed. +Lemma Z_quot_le_lower_bound : forall a b q : Z, 0 < b -> b * q <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_le_mono : forall a b c : Z, 0 < c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma Z_quot_le_upper_bound : forall a b q : Z, 0 < b -> a <= b * q -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma Z_quot_lt : forall a b : Z, 0 < a -> 1 < b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma Z_quot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < b * q -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma Z_quot_mul_cancel_l : forall a b c : Z, b <> 0 -> c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_mul_cancel_r : forall a b c : Z, b <> 0 -> c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_mul : forall a b : Z, b <> 0 -> a * b ÷ b = a. Proof. intros; nia. Qed. +Lemma Z_quot_mul_le : forall a b c : Z, 0 <= a -> 0 < b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_opp_l : forall a b : Z, b <> 0 -> - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_quot_opp_opp : forall a b : Z, b <> 0 -> - a ÷ - b = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_opp_r : forall a b : Z, b <> 0 -> a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_quot_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_quot : forall a b c : Z, b <> 0 -> c <> 0 -> a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma Z_quot_rem' : forall a b : Z, a = b * (a ÷ b) + Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_quot_rem : forall a b : Z, b <> 0 -> a = b * (a ÷ b) + Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_quot_same : forall a : Z, a <> 0 -> a ÷ a = 1. Proof. intros; nia. Qed. +Lemma Z_quot_small : forall a b : Z, 0 <= a < b -> a ÷ b = 0. Proof. intros; nia. Qed. +Lemma Z_quot_small_iff : forall a b : Z, b <> 0 -> a ÷ b = 0 <-> Z.abs a < Z.abs b. Proof. intros; nia. Qed. +Lemma Z_quot_str_pos : forall a b : Z, 0 < b <= a -> 0 < a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_unique_exact : forall a b q : Z, b <> 0 -> a = b * q -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma Z_quot_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Z_quot_wd Morphisms.Proper (Morphisms.respectful Z.eq (Morphisms.respectful Z.eq Z.eq)) Z.quot +Lemma Zquot_Zeven_rem : forall a : Z, Z.even a = (Z.rem a 2 =? 0). Proof. intros; nia. Qed. +Lemma Zquot_Z_mult_quot_ge : forall a b : Z, a <= 0 -> a <= b * (a ÷ b) <= 0. Proof. intros; nia. Qed. +Lemma Zquot_Z_mult_quot_le : forall a b : Z, 0 <= a -> 0 <= b * (a ÷ b) <= a. Proof. intros; nia. Qed. +Lemma Zquot_Zmult_rem_distr_l : forall a b c : Z, Z.rem (c * a) (c * b) = c * Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Zmult_rem_distr_r : forall a b c : Z, Z.rem (a * c) (b * c) = Z.rem a b * c. Proof. intros; nia. Qed. +Lemma Zquot_Zmult_rem : forall a b n : Z, Z.rem (a * b) n = Z.rem (Z.rem a n * Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Zquot_Zmult_rem_idemp_l : forall a b n : Z, Z.rem (Z.rem a n * b) n = Z.rem (a * b) n. Proof. intros; nia. Qed. +Lemma Zquot_Zmult_rem_idemp_r : forall a b n : Z, Z.rem (b * Z.rem a n) n = Z.rem (b * a) n. Proof. intros; nia. Qed. +Lemma Zquot_Zodd_rem : forall a : Z, Z.odd a = negb (Z.rem a 2 =? 0). Proof. intros; nia. Qed. +Lemma Zquot_Zplus_rem : forall a b n : Z, 0 <= a * b -> Z.rem (a + b) n = Z.rem (Z.rem a n + Z.rem b n) n. Proof. intros; nia. Qed. +Lemma Zquot_Zplus_rem_idemp_l : forall a b n : Z, 0 <= a * b -> Z.rem (Z.rem a n + b) n = Z.rem (a + b) n. Proof. intros; nia. Qed. +Lemma Zquot_Zplus_rem_idemp_r : forall a b n : Z, 0 <= a * b -> Z.rem (b + Z.rem a n) n = Z.rem (b + a) n. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_0_l : forall a : Z, 0 ÷ a = 0. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_0_r : forall a : Z, a ÷ 0 = 0. Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_exact_full : forall a b : Z, a = b * (a ÷ b) <-> Z.rem a b = 0. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_le_lower_bound : forall a b q : Z, 0 < b -> q * b <= a -> q <= a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_le_upper_bound : forall a b q : Z, 0 < b -> a <= q * b -> a ÷ b <= q. Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_lt : forall a b : Z, 0 < a -> 2 <= b -> a ÷ b < a. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_lt_upper_bound : forall a b q : Z, 0 <= a -> 0 < b -> a < q * b -> a ÷ b < q. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_mod_unique_full : forall a b q r : Z, Zquot.Remainder a b r -> a = b * q + r -> q = a ÷ b /\ r = Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_monotone : forall a b c : Z, 0 <= c -> a <= b -> a ÷ c <= b ÷ c. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_mult_cancel_l : forall a b c : Z, c <> 0 -> c * a ÷ (c * b) = a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_mult_cancel_r : forall a b c : Z, c <> 0 -> a * c ÷ (b * c) = a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_mult_le : forall a b c : Z, 0 <= a -> 0 <= b -> 0 <= c -> c * (a ÷ b) <= c * a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_opp_l : forall a b : Z, - a ÷ b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma Zquot_Zquot_opp_opp : forall a b : Z, - a ÷ - b = a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_opp_r : forall a b : Z, a ÷ - b = - (a ÷ b). Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_plus : forall a b c : Z, 0 <= (a + b * c) * a -> c <> 0 -> (a + b * c) ÷ c = a ÷ c + b. Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_plus_l : forall a b c : Z, 0 <= (a * b + c) * c -> b <> 0 -> b <> 0 -> (a * b + c) ÷ b = a + c ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Z_quot_pos : forall a b : Z, 0 <= a -> 0 <= b -> 0 <= a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquotrem_Zdiv_eucl_pos : forall a b : Z, 0 <= a -> 0 < b -> a ÷ b = a / b /\ Z.rem a b = a mod b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_sgn : forall a b : Z, 0 <= Z.sgn (a ÷ b) * Z.sgn a * Z.sgn b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_unique_full : forall a b q r : Z, Zquot.Remainder a b r -> a = b * q + r -> q = a ÷ b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_Zdiv_pos : forall a b : Z, 0 <= a -> 0 <= b -> a ÷ b = a / b. Proof. intros; nia. Qed. +Lemma Zquot_Zquot_Zquot : forall a b c : Z, a ÷ b ÷ c = a ÷ (b * c). Proof. intros; nia. Qed. +Lemma Zquot_Zrem_0_l : forall a : Z, Z.rem 0 a = 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_0_r : forall a : Z, Z.rem a 0 = a. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_divides : forall a b : Z, Z.rem a b = 0 <-> (exists c : Z, a = b * c). Proof. intros; nia. Qed. +Lemma Zquot_Zrem_even : forall a : Z, Z.rem a 2 = (if Z.even a then 0 else Z.sgn a). Proof. intros; nia. Qed. +Lemma Zquot_Zrem_le : forall a b : Z, 0 <= a -> 0 <= b -> Z.rem a b <= a. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_neg : forall a b : Z, a <= 0 -> b <> 0 -> - Z.abs b < Z.rem a b <= 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_neg_neg : forall a b : Z, a <= 0 -> b < 0 -> b < Z.rem a b <= 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_neg_pos : forall a b : Z, a <= 0 -> 0 < b -> - b < Z.rem a b <= 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_pos : forall a b : Z, 0 <= a -> b <> 0 -> 0 <= Z.rem a b < Z.abs b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_pos_neg : forall a b : Z, 0 <= a -> b < 0 -> 0 <= Z.rem a b < - b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_lt_pos_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= Z.rem a b < b. Proof. intros; nia. Qed. +Lemma Zquot_Z_rem_mult : forall a b : Z, Z.rem (a * b) b = 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_odd : forall a : Z, Z.rem a 2 = (if Z.odd a then Z.sgn a else 0). Proof. intros; nia. Qed. +Lemma Zquot_Zrem_opp_l : forall a b : Z, Z.rem (- a) b = - Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_opp_opp : forall a b : Z, Z.rem (- a) (- b) = - Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_opp_r : forall a b : Z, Z.rem a (- b) = Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Z_rem_plus : forall a b c : Z, 0 <= (a + b * c) * a -> Z.rem (a + b * c) c = Z.rem a c. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_rem : forall a n : Z, Z.rem (Z.rem a n) n = Z.rem a n. Proof. intros; nia. Qed. +Lemma Zquot_Z_rem_same : forall a : Z, Z.rem a a = 0. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_sgn2 : forall a b : Z, 0 <= Z.rem a b * a. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_sgn : forall a b : Z, 0 <= Z.sgn (Z.rem a b) * Z.sgn a. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_unique_full : forall a b q r : Z, Zquot.Remainder a b r -> a = b * q + r -> r = Z.rem a b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_Zmod_pos : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = a mod b. Proof. intros; nia. Qed. +Lemma Zquot_Zrem_Zmod_zero : forall a b : Z, b <> 0 -> Z.rem a b = 0 <-> a mod b = 0. Proof. intros; nia. Qed. +Lemma Z_rem_0_l : forall a : Z, a <> 0 -> Z.rem 0 a = 0. Proof. intros; nia. Qed. +Lemma Z_rem_0_r_ext : forall x y : Z, y = 0 -> Z.rem x y = x. Proof. intros; nia. Qed. +Lemma Z_rem_1_l : forall a : Z, 1 < a -> Z.rem 1 a = 1. Proof. intros; nia. Qed. +Lemma Z_rem_1_r : forall a : Z, Z.rem a 1 = 0. Proof. intros; nia. Qed. +Lemma Z_rem_abs : forall a b : Z, b <> 0 -> Z.rem (Z.abs a) (Z.abs b) = Z.abs (Z.rem a b). Proof. intros; nia. Qed. +Lemma Z_rem_abs_l : forall a b : Z, b <> 0 -> Z.rem (Z.abs a) b = Z.abs (Z.rem a b). Proof. intros; nia. Qed. +Lemma Z_rem_abs_r : forall a b : Z, b <> 0 -> Z.rem a (Z.abs b) = Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_add : forall a b c : Z, c <> 0 -> 0 <= (a + b * c) * a -> Z.rem (a + b * c) c = Z.rem a c. Proof. intros; nia. Qed. +Lemma Z_rem_bound_abs : forall a b : Z, b <> 0 -> Z.abs (Z.rem a b) < Z.abs b. Proof. intros; nia. Qed. +Lemma Z_rem_bound_neg_neg : forall x y : Z, y < 0 -> x <= 0 -> y < Z.rem x y <= 0. Proof. intros; nia. Qed. +Lemma Z_rem_bound_neg_pos : forall x y : Z, y < 0 -> 0 <= x -> 0 <= Z.rem x y < - y. Proof. intros; nia. Qed. +Lemma Z_rem_bound_pos : forall a b : Z, 0 <= a -> 0 < b -> 0 <= Z.rem a b < b. Proof. intros; nia. Qed. +Lemma Z_rem_bound_pos_neg : forall x y : Z, 0 < y -> x <= 0 -> - y < Z.rem x y <= 0. Proof. intros; nia. Qed. +Lemma Z_rem_bound_pos_pos : forall x y : Z, 0 < y -> 0 <= x -> 0 <= Z.rem x y < y. Proof. intros; nia. Qed. +Lemma Z_rem_eq : forall a b : Z, b <> 0 -> Z.rem a b = a - b * (a ÷ b). Proof. intros; nia. Qed. +Lemma Z_rem_le : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b <= a. Proof. intros; nia. Qed. +Lemma Z_rem_mod_eq_0 : forall a b : Z, b <> 0 -> Z.rem a b = 0 <-> a mod b = 0. Proof. intros; nia. Qed. +Lemma Z_rem_mod : forall a b : Z, b <> 0 -> Z.rem a b = Z.sgn a * (Z.abs a mod Z.abs b). Proof. intros; nia. Qed. +Lemma Z_rem_mod_nonneg : forall a b : Z, 0 <= a -> 0 < b -> Z.rem a b = a mod b. Proof. intros; nia. Qed. +Lemma Z_rem_mul : forall a b : Z, b <> 0 -> Z.rem (a * b) b = 0. Proof. intros; nia. Qed. +Lemma Z_rem_nonneg : forall a b : Z, b <> 0 -> 0 <= a -> 0 <= Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_nonpos : forall a b : Z, b <> 0 -> a <= 0 -> Z.rem a b <= 0. Proof. intros; nia. Qed. +Lemma Z_rem_opp_l : forall a b : Z, b <> 0 -> Z.rem (- a) b = - Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_opp_l' : forall a b : Z, Z.rem (- a) b = - Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_opp_opp : forall a b : Z, b <> 0 -> Z.rem (- a) (- b) = - Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_opp_r : forall a b : Z, b <> 0 -> Z.rem a (- b) = Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_opp_r' : forall a b : Z, Z.rem a (- b) = Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_quot : forall a b : Z, b <> 0 -> Z.rem a b ÷ b = 0. Proof. intros; nia. Qed. +Lemma Z_rem_rem : forall a n : Z, n <> 0 -> Z.rem (Z.rem a n) n = Z.rem a n. Proof. intros; nia. Qed. +Lemma Z_rem_same : forall a : Z, a <> 0 -> Z.rem a a = 0. Proof. intros; nia. Qed. +Lemma Z_rem_sign : forall a b : Z, a <> 0 -> b <> 0 -> Z.sgn (Z.rem a b) <> - Z.sgn a. Proof. intros; nia. Qed. +Lemma Z_rem_sign_mul : forall a b : Z, b <> 0 -> 0 <= Z.rem a b * a. Proof. intros; nia. Qed. +Lemma Z_rem_sign_nz : forall a b : Z, b <> 0 -> Z.rem a b <> 0 -> Z.sgn (Z.rem a b) = Z.sgn a. Proof. intros; nia. Qed. +Lemma Z_rem_small : forall a b : Z, 0 <= a < b -> Z.rem a b = a. Proof. intros; nia. Qed. +Lemma Z_rem_small_iff : forall a b : Z, b <> 0 -> Z.rem a b = a <-> Z.abs a < Z.abs b. Proof. intros; nia. Qed. +Lemma Z_rem_unique : forall a b q r : Z, 0 <= a -> 0 <= r < b -> a = b * q + r -> r = Z.rem a b. Proof. intros; nia. Qed. +Lemma Z_rem_wd : Morphisms.Proper (Morphisms.respectful Z.eq (Morphisms.respectful Z.eq Z.eq)) Z.rem. Proof. intros; nia. Qed. +*) |