https://github.com/uds-psl/cook-levin
Tip revision: e24a92af25746f6758a09ea1dc51e57491508e60 authored by Fabian Kunze on 03 February 2021, 23:29:51 UTC
added missing html doc
added missing html doc
Tip revision: e24a92a
Complexity.Complexity.ONotation.html
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="config.js"></script>
<script type="text/javascript" src="coqdocjs.js"></script>
</head>
<body onload="document.getElementById('content').focus()">
<div id="header">
<span class="left">
<span class="modulename"> <script> document.write(document.title) </script> </span>
</span>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="../">Project Page</a>
<a href="./indexpage.html"> Index </a>
<a href="./toc.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
<div class="code">
<span class="id" title="keyword">From</span> <span class="id" title="var">Undecidability</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.Shared.Libs.PSL.Prelim.html#"><span class="id" title="library">PSL.Prelim</span></a> <a class="idref" href="Undecidability.L.Prelim.MoreBase.html#"><span class="id" title="library">L.Prelim.MoreBase</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Complexity.Complexity</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Complexity.Complexity.Monotonic.html#"><span class="id" title="library">Monotonic</span></a>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">smpl.Smpl</span>.<br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Nat.html#"><span class="id" title="library">Nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.micromega.Lia.html#"><span class="id" title="library">Lia</span></a>.<br/>
<br/>
</div>
<div class="doc">
<a id="lab9"></a><h2 class="section">O notation</h2>
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a id="inO" class="idref" href="#inO"><span class="id" title="definition">inO</span></a> (<a id="f:1" class="idref" href="#f:1"><span class="id" title="binder">f</span></a> <a id="g:2" class="idref" href="#g:2"><span class="id" title="binder">g</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <span class="id" title="keyword">Prop</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">exists</span></a> <a id="c:3" class="idref" href="#c:3"><span class="id" title="binder">c</span></a> <a id="n0:4" class="idref" href="#n0:4"><span class="id" title="binder">n0</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">forall</span> <a id="n:5" class="idref" href="#n:5"><span class="id" title="binder">n</span></a>, <a class="idref" href="Complexity.Complexity.ONotation.html#n0:4"><span class="id" title="variable">n0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation"><=</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:5"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f:1"><span class="id" title="variable">f</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:5"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation"><=</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#c:3"><span class="id" title="variable">c</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:2"><span class="id" title="variable">g</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:5"><span class="id" title="variable">n</span></a>.<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a id="fb13635db5891cd876d35f6ab833523d" class="idref" href="#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">"</span></a> f ∈O g" := (<a class="idref" href="Complexity.Complexity.ONotation.html#inO"><span class="id" title="definition">inO</span></a> <span class="id" title="var">f</span> <span class="id" title="var">g</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70).<br/>
<br/>
<span class="id" title="keyword">Instance</span> <a id="inO_PreOrder" class="idref" href="#inO_PreOrder"><span class="id" title="instance">inO_PreOrder</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.RelationClasses.html#PreOrder"><span class="id" title="class">PreOrder</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#inO"><span class="id" title="definition">inO</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">split</span>.<br/>
-<span class="id" title="tactic">exists</span> 1,0. <span class="id" title="tactic">intros</span>. <span class="id" title="var">Lia.lia</span>.<br/>
-<span class="id" title="tactic">intros</span> <span class="id" title="var">f</span> <span class="id" title="var">g</span> <span class="id" title="var">h</span> (<span class="id" title="var">c</span>&<span class="id" title="var">n0</span>&<span class="id" title="var">H</span>) (<span class="id" title="var">c'</span>&<span class="id" title="var">n0'</span>&<span class="id" title="var">H'</span>).<br/>
<span class="id" title="tactic">exists</span> (<span class="id" title="var">c</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a><span class="id" title="var">c'</span>),(<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Nat.html#max"><span class="id" title="definition">max</span></a> <span class="id" title="var">n0</span> <span class="id" title="var">n0'</span>).<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span> <span class="id" title="var">Hn</span>.<br/>
<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H</span>,<span class="id" title="var">H'</span>. <span class="id" title="var">all</span>:<span class="id" title="var">Lia.lia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Instance</span> <a id="inO_pointwise_leq" class="idref" href="#inO_pointwise_leq"><span class="id" title="instance">inO_pointwise_leq</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#Proper"><span class="id" title="class">Proper</span></a> ( <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Program.Basics.html#flip"><span class="id" title="definition">Basics.flip</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#pointwise_relation"><span class="id" title="definition">pointwise_relation</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#le"><span class="id" title="inductive">le</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">==></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#pointwise_relation"><span class="id" title="definition">pointwise_relation</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#le"><span class="id" title="inductive">le</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">==></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Program.Basics.html#impl"><span class="id" title="definition">Basics.impl</span></a>) <a class="idref" href="Complexity.Complexity.ONotation.html#inO"><span class="id" title="definition">inO</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> ? ? <span class="id" title="var">R1</span> ? ? <span class="id" title="var">R2</span>. <span class="id" title="tactic">unfold</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO"><span class="id" title="definition">inO</span></a>. <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <span class="id" title="var">R1</span>,<span class="id" title="var">R2</span>|-*.<br/>
<span class="id" title="tactic">setoid_rewrite</span> <span class="id" title="var">R1</span>. <span class="id" title="tactic">setoid_rewrite</span> <span class="id" title="var">R2</span>. <span class="id" title="var">easy</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Instance</span> <a id="inO_pointwise_eq" class="idref" href="#inO_pointwise_eq"><span class="id" title="instance">inO_pointwise_eq</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#Proper"><span class="id" title="class">Proper</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#pointwise_relation"><span class="id" title="definition">pointwise_relation</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#eq"><span class="id" title="inductive">eq</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">==></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#pointwise_relation"><span class="id" title="definition">pointwise_relation</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#eq"><span class="id" title="inductive">eq</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">==></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#iff"><span class="id" title="definition">iff</span></a>) <a class="idref" href="Complexity.Complexity.ONotation.html#inO"><span class="id" title="definition">inO</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> ? ? <span class="id" title="var">R1</span> ? ? <span class="id" title="var">R2</span>. <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <span class="id" title="var">R1</span>,<span class="id" title="var">R2</span>.<br/>
<span class="id" title="tactic">unfold</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO"><span class="id" title="definition">inO</span></a>. <span class="id" title="tactic">setoid_rewrite</span> <span class="id" title="var">R1</span>. <span class="id" title="tactic">setoid_rewrite</span> <span class="id" title="var">R2</span>. <span class="id" title="var">easy</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inO_add_l" class="idref" href="#inO_add_l"><span class="id" title="lemma">inO_add_l</span></a> <a id="f1:6" class="idref" href="#f1:6"><span class="id" title="binder">f1</span></a> <a id="f2:7" class="idref" href="#f2:7"><span class="id" title="binder">f2</span></a> <a id="g:8" class="idref" href="#g:8"><span class="id" title="binder">g</span></a>:<br/>
<a class="idref" href="Complexity.Complexity.ONotation.html#f1:6"><span class="id" title="variable">f1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:8"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f2:7"><span class="id" title="variable">f2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:8"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">fun</span> <a id="n:9" class="idref" href="#n:9"><span class="id" title="binder">n</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#f1:6"><span class="id" title="variable">f1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:9"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f2:7"><span class="id" title="variable">f2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:9"><span class="id" title="variable">n</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">)</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:8"><span class="id" title="variable">g</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> (<span class="id" title="var">c1</span>&<span class="id" title="var">n1</span>&<span class="id" title="var">H1</span>) (<span class="id" title="var">c2</span>&<span class="id" title="var">n2</span>&<span class="id" title="var">H2</span>).<br/>
<span class="id" title="tactic">eexists</span> (<span class="id" title="var">c1</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <span class="id" title="var">c2</span>),(<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Nat.html#max"><span class="id" title="definition">max</span></a> <span class="id" title="var">n1</span> <span class="id" title="var">n2</span>).<br/>
<span class="id" title="tactic">intros</span>.<br/>
<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H1</span>,<span class="id" title="var">H2</span>.<br/>
<span class="id" title="var">all</span>:<span class="id" title="var">Lia.lia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inO_mul_c_l" class="idref" href="#inO_mul_c_l"><span class="id" title="lemma">inO_mul_c_l</span></a> <a id="c:10" class="idref" href="#c:10"><span class="id" title="binder">c</span></a> <a id="f1:11" class="idref" href="#f1:11"><span class="id" title="binder">f1</span></a> <a id="g:12" class="idref" href="#g:12"><span class="id" title="binder">g</span></a>:<br/>
<a class="idref" href="Complexity.Complexity.ONotation.html#f1:11"><span class="id" title="variable">f1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:12"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">fun</span> <a id="n:13" class="idref" href="#n:13"><span class="id" title="binder">n</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#c:10"><span class="id" title="variable">c</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f1:11"><span class="id" title="variable">f1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:13"><span class="id" title="variable">n</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">)</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:12"><span class="id" title="variable">g</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> (<span class="id" title="var">c1</span>&<span class="id" title="var">n1</span>&<span class="id" title="var">H1</span>).<br/>
<span class="id" title="tactic">eexists</span> (<span class="id" title="var">c1</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a><span class="id" title="var">c</span>), (<span class="id" title="var">n1</span>).<br/>
<span class="id" title="tactic">intros</span>.<br/>
<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H1</span>.<br/>
<span class="id" title="var">all</span>:<span class="id" title="var">Lia.lia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inO_mul_c_r" class="idref" href="#inO_mul_c_r"><span class="id" title="lemma">inO_mul_c_r</span></a> <a id="c:14" class="idref" href="#c:14"><span class="id" title="binder">c</span></a> <a id="f1:15" class="idref" href="#f1:15"><span class="id" title="binder">f1</span></a> <a id="g:16" class="idref" href="#g:16"><span class="id" title="binder">g</span></a>:<br/>
<a class="idref" href="Complexity.Complexity.ONotation.html#f1:15"><span class="id" title="variable">f1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:16"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">fun</span> <a id="n:17" class="idref" href="#n:17"><span class="id" title="binder">n</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#f1:15"><span class="id" title="variable">f1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:17"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#c:14"><span class="id" title="variable">c</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">)</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:16"><span class="id" title="variable">g</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> (<span class="id" title="var">c1</span>&<span class="id" title="var">n1</span>&<span class="id" title="var">H1</span>).<br/>
<span class="id" title="tactic">eexists</span> (<span class="id" title="var">c1</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a><span class="id" title="var">c</span>),(<span class="id" title="var">n1</span>).<br/>
<span class="id" title="tactic">intros</span>.<br/>
<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H1</span>.<br/>
<span class="id" title="var">all</span>:<span class="id" title="var">Lia.lia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inO_c" class="idref" href="#inO_c"><span class="id" title="lemma">inO_c</span></a> <a id="c:18" class="idref" href="#c:18"><span class="id" title="binder">c</span></a> <a id="f':19" class="idref" href="#f':19"><span class="id" title="binder">f'</span></a>:<br/>
<a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> => 1<a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">)</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f':19"><span class="id" title="variable">f'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <br/>
<a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> => <a class="idref" href="Complexity.Complexity.ONotation.html#c:18"><span class="id" title="variable">c</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">)</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f':19"><span class="id" title="variable">f'</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">H'</span>.<br/>
<span class="id" title="tactic">assert</span> (<span class="id" title="var">H</span>:<span class="id" title="var">c</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation"><=</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a><span class="id" title="var">c</span>) <span class="id" title="tactic">by</span> <span class="id" title="var">lia</span>.<br/>
<span class="id" title="tactic">setoid_rewrite</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_mul_c_r"><span class="id" title="lemma">inO_mul_c_r</span></a>. <span class="id" title="var">easy</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inO_leq" class="idref" href="#inO_leq"><span class="id" title="lemma">inO_leq</span></a> <a id="n0:20" class="idref" href="#n0:20"><span class="id" title="binder">n0</span></a> <a id="f':21" class="idref" href="#f':21"><span class="id" title="binder">f'</span></a> <a id="g:22" class="idref" href="#g:22"><span class="id" title="binder">g</span></a>:<br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">forall</span> <a id="n':23" class="idref" href="#n':23"><span class="id" title="binder">n'</span></a>, <a class="idref" href="Complexity.Complexity.ONotation.html#n0:20"><span class="id" title="variable">n0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation"><=</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n':23"><span class="id" title="variable">n'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f':21"><span class="id" title="variable">f'</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n':23"><span class="id" title="variable">n'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation"><=</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:22"><span class="id" title="variable">g</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n':23"><span class="id" title="variable">n'</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <br/>
<a class="idref" href="Complexity.Complexity.ONotation.html#f':21"><span class="id" title="variable">f'</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:22"><span class="id" title="variable">g</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">eexists</span> 1,(<span class="id" title="var">n0</span>).<br/>
<span class="id" title="tactic">intros</span>. <span class="id" title="tactic">rewrite</span> <- <span class="id" title="var">H</span>. <span class="id" title="var">all</span>:<span class="id" title="var">Lia.nia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="var">Smpl</span> <span class="id" title="var">Create</span> <span class="id" title="var">inO</span>.<br/>
<br/>
<span class="id" title="var">Smpl</span> <span class="id" title="keyword">Add</span> 11 (<span class="id" title="var">smpl</span> <span class="id" title="var">monotonic</span>) : <span class="id" title="var">inO</span>.<br/>
<br/>
<span class="id" title="var">Smpl</span> <span class="id" title="keyword">Add</span> 10 (<span class="id" title="tactic">first</span> [ <span class="id" title="tactic">simple</span> <span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_add_l"><span class="id" title="lemma">inO_add_l</span></a> | <span class="id" title="tactic">simple</span> <span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_mul_c_l"><span class="id" title="lemma">inO_mul_c_l</span></a> | <span class="id" title="tactic">simple</span> <span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_mul_c_r"><span class="id" title="lemma">inO_mul_c_r</span></a> | <span class="id" title="tactic">progress</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_c"><span class="id" title="lemma">inO_c</span></a>) | <span class="id" title="tactic">reflexivity</span>]) : <span class="id" title="var">inO</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">smpl_inO</span> := <span class="id" title="tactic">repeat</span> (<span class="id" title="var">smpl</span> <span class="id" title="var">inO</span>).<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inO_mul_l" class="idref" href="#inO_mul_l"><span class="id" title="lemma">inO_mul_l</span></a> <a id="f1:24" class="idref" href="#f1:24"><span class="id" title="binder">f1</span></a> <a id="f2:25" class="idref" href="#f2:25"><span class="id" title="binder">f2</span></a> <a id="g1:26" class="idref" href="#g1:26"><span class="id" title="binder">g1</span></a> <a id="g2:27" class="idref" href="#g2:27"><span class="id" title="binder">g2</span></a>:<br/>
<a class="idref" href="Complexity.Complexity.ONotation.html#f1:24"><span class="id" title="variable">f1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g1:26"><span class="id" title="variable">g1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f2:25"><span class="id" title="variable">f2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g2:27"><span class="id" title="variable">g2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">fun</span> <a id="n:28" class="idref" href="#n:28"><span class="id" title="binder">n</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#f1:24"><span class="id" title="variable">f1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:28"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f2:25"><span class="id" title="variable">f2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:28"><span class="id" title="variable">n</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">)</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">fun</span> <a id="n:29" class="idref" href="#n:29"><span class="id" title="binder">n</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#g1:26"><span class="id" title="variable">g1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:29"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g2:27"><span class="id" title="variable">g2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:29"><span class="id" title="variable">n</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> (<span class="id" title="var">c1</span>&<span class="id" title="var">n1</span>&<span class="id" title="var">H1</span>) (<span class="id" title="var">c2</span>&<span class="id" title="var">n2</span>&<span class="id" title="var">H2</span>).<br/>
<span class="id" title="tactic">eexists</span> (<span class="id" title="var">c1</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <span class="id" title="var">c2</span>),(<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Nat.html#max"><span class="id" title="definition">max</span></a> <span class="id" title="var">n1</span> <span class="id" title="var">n2</span>).<br/>
<span class="id" title="tactic">intros</span>.<br/>
<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H1</span>,<span class="id" title="var">H2</span>.<br/>
<span class="id" title="var">all</span>:<span class="id" title="var">Lia.lia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inO_comp_l" class="idref" href="#inO_comp_l"><span class="id" title="lemma">inO_comp_l</span></a> <a id="f1:30" class="idref" href="#f1:30"><span class="id" title="binder">f1</span></a> <a id="f2:31" class="idref" href="#f2:31"><span class="id" title="binder">f2</span></a> <a id="g1:32" class="idref" href="#g1:32"><span class="id" title="binder">g1</span></a> <a id="g2:33" class="idref" href="#g2:33"><span class="id" title="binder">g2</span></a>:<br/>
<a class="idref" href="Complexity.Complexity.ONotation.html#f1:30"><span class="id" title="variable">f1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g1:32"><span class="id" title="variable">g1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f2:31"><span class="id" title="variable">f2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g2:33"><span class="id" title="variable">g2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a><br/>
<a class="idref" href="Complexity.Complexity.Monotonic.html#monotonic"><span class="id" title="definition">monotonic</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f1:30"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">forall</span> <a id="x:38" class="idref" href="#x:38"><span class="id" title="binder">x</span></a>, <a class="idref" href="Complexity.Complexity.ONotation.html#x:38"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation"><=</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g2:33"><span class="id" title="variable">g2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#x:38"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a><br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">forall</span> <a id="c:36" class="idref" href="#c:36"><span class="id" title="binder">c</span></a>, <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">fun</span> <a id="x:37" class="idref" href="#x:37"><span class="id" title="binder">x</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#g1:32"><span class="id" title="variable">g1</span></a> (<a class="idref" href="Complexity.Complexity.ONotation.html#c:36"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#x:37"><span class="id" title="variable">x</span></a>)<a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">)</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g1:32"><span class="id" title="variable">g1</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">fun</span> <a id="n:34" class="idref" href="#n:34"><span class="id" title="binder">n</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#f1:30"><span class="id" title="variable">f1</span></a> (<a class="idref" href="Complexity.Complexity.ONotation.html#f2:31"><span class="id" title="variable">f2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:34"><span class="id" title="variable">n</span></a>)<a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">)</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">fun</span> <a id="n:35" class="idref" href="#n:35"><span class="id" title="binder">n</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#g1:32"><span class="id" title="variable">g1</span></a> (<a class="idref" href="Complexity.Complexity.ONotation.html#g2:33"><span class="id" title="variable">g2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:35"><span class="id" title="variable">n</span></a>)<a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> (<span class="id" title="var">c1</span>&<span class="id" title="var">n1</span>&<span class="id" title="var">H1</span>) (<span class="id" title="var">c2</span>&<span class="id" title="var">n2</span>&<span class="id" title="var">H2</span>) <span class="id" title="var">mono2</span> <span class="id" title="var">H'</span> <span class="id" title="var">H</span>.<br/>
<span class="id" title="tactic">specialize</span> (<span class="id" title="var">H</span> (<span class="id" title="var">c2</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a><span class="id" title="var">n1</span>)) <span class="id" title="keyword">as</span> (<span class="id" title="var">c2'</span>&<span class="id" title="var">n2'</span>&<span class="id" title="var">H</span>).<br/>
<span class="id" title="tactic">eexists</span> (<span class="id" title="var">c1</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <span class="id" title="var">c2'</span>),(<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Nat.html#max"><span class="id" title="definition">max</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Nat.html#max"><span class="id" title="definition">max</span></a> 1 <span class="id" title="var">n2'</span>) <span class="id" title="var">n2</span>).<br/>
<span class="id" title="tactic">intros</span>.<br/>
<span class="id" title="var">etransitivity</span>.<br/>
{<span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <span class="id" title="var">mono2</span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">mono2</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="tactic">transitivity</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">(</span></a><span class="id" title="var">c2</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a><span class="id" title="var">n1</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">)*(</span></a><span class="id" title="var">g2</span> <span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">)</span></a>). 2:<span class="id" title="tactic">reflexivity</span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">H2</span>. <span class="id" title="var">Lia.nia</span>. <span class="id" title="var">lia</span>. }<br/>
<span class="id" title="tactic">specialize</span> (<span class="id" title="var">H'</span> <span class="id" title="var">n</span>).<br/>
<span class="id" title="tactic">setoid_rewrite</span> <span class="id" title="var">H1</span>. 2:<span class="id" title="var">Lia.nia</span>.<br/>
<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H</span>. <span class="id" title="var">Lia.nia</span>. <span class="id" title="var">Lia.nia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inO__bound" class="idref" href="#inO__bound"><span class="id" title="lemma">inO__bound</span></a> <a id="f:39" class="idref" href="#f:39"><span class="id" title="binder">f</span></a> <a id="g:40" class="idref" href="#g:40"><span class="id" title="binder">g</span></a> (<a id="H:41" class="idref" href="#H:41"><span class="id" title="binder">H</span></a>:<a class="idref" href="Complexity.Complexity.ONotation.html#f:39"><span class="id" title="variable">f</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:40"><span class="id" title="variable">g</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">exists</span></a> <a id="c:42" class="idref" href="#c:42"><span class="id" title="binder">c</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">forall</span> <a id="n:43" class="idref" href="#n:43"><span class="id" title="binder">n</span></a>, <a class="idref" href="Complexity.Complexity.ONotation.html#f:39"><span class="id" title="variable">f</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:43"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation"><=</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#c:42"><span class="id" title="variable">c</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#c:42"><span class="id" title="variable">c</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:40"><span class="id" title="variable">g</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:43"><span class="id" title="variable">n</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">destruct</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> (<span class="id" title="var">c0</span>&<span class="id" title="var">n0</span>&<span class="id" title="var">H</span>). <span class="id" title="var">cbn</span>.<br/>
<span class="id" title="tactic">exists</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Nat.html#max"><span class="id" title="definition">max</span></a> <span class="id" title="var">c0</span> (<a class="idref" href="Undecidability.L.Prelim.MoreList.html#maxl"><span class="id" title="definition">maxl</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#map"><span class="id" title="definition">map</span></a> <span class="id" title="var">f</span> (<a class="idref" href="Undecidability.L.Prelim.MoreList.html#natsLess"><span class="id" title="definition">natsLess</span></a> <span class="id" title="var">n0</span>)))).<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">n</span>.<br/>
<span class="id" title="var">decide</span> (<span class="id" title="var">n0</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation"><=</span></a><span class="id" title="var">n</span>).<br/>
-<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H</span>. <span class="id" title="var">all</span>:<span class="id" title="var">Lia.nia</span>.<br/>
-<span class="id" title="tactic">rewrite</span> (@<a class="idref" href="Undecidability.L.Prelim.MoreList.html#maxl_leq"><span class="id" title="lemma">maxl_leq</span></a> (<span class="id" title="var">f</span> <span class="id" title="var">n</span>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#map"><span class="id" title="definition">map</span></a> <span class="id" title="var">f</span> (<a class="idref" href="Undecidability.L.Prelim.MoreList.html#natsLess"><span class="id" title="definition">natsLess</span></a> <span class="id" title="var">n0</span>))). <span class="id" title="var">Lia.nia</span>. <span class="id" title="tactic">apply</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Lists.List.html#in_map_iff"><span class="id" title="lemma">in_map_iff</span></a>. <span class="id" title="tactic">setoid_rewrite</span> <a class="idref" href="Undecidability.L.Prelim.MoreList.html#natsLess_in_iff"><span class="id" title="lemma">natsLess_in_iff</span></a>. <span class="id" title="tactic">exists</span> <span class="id" title="var">n</span>. <span class="id" title="tactic">intuition</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a id="lab10"></a><h3 class="section">smallO</h3>
<div class="paragraph"> </div>
This variant of smallo does not need real nubers, as we moved the constant to the other side
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a id="ino" class="idref" href="#ino"><span class="id" title="definition">ino</span></a> (<a id="f:44" class="idref" href="#f:44"><span class="id" title="binder">f</span></a> <a id="g:45" class="idref" href="#g:45"><span class="id" title="binder">g</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <span class="id" title="keyword">Prop</span> := <span class="id" title="keyword">forall</span> <a id="c__inv:46" class="idref" href="#c__inv:46"><span class="id" title="binder">c__inv</span></a>, <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">exists</span></a> <a id="n0:47" class="idref" href="#n0:47"><span class="id" title="binder">n0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">forall</span> <a id="n:48" class="idref" href="#n:48"><span class="id" title="binder">n</span></a>, <a class="idref" href="Complexity.Complexity.ONotation.html#n0:47"><span class="id" title="variable">n0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation"><=</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:48"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#c__inv:46"><span class="id" title="variable">c__inv</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f:44"><span class="id" title="variable">f</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:48"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#::nat_scope:x_'<'_x"><span class="id" title="notation"><</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:45"><span class="id" title="variable">g</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:48"><span class="id" title="variable">n</span></a>.<br/>
<br/>
<span class="id" title="keyword">Notation</span> <a id="4806e03a8439f8521169dfc83e768cdb" class="idref" href="#4806e03a8439f8521169dfc83e768cdb"><span class="id" title="notation">"</span></a> f ∈o g" := (<a class="idref" href="Complexity.Complexity.ONotation.html#ino"><span class="id" title="definition">ino</span></a> <span class="id" title="var">f</span> <span class="id" title="var">g</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70).<br/>
<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="ino_inO_incl" class="idref" href="#ino_inO_incl"><span class="id" title="lemma">ino_inO_incl</span></a> <a id="f:49" class="idref" href="#f:49"><span class="id" title="binder">f</span></a> <a id="g:50" class="idref" href="#g:50"><span class="id" title="binder">g</span></a> :<br/>
<a class="idref" href="Complexity.Complexity.ONotation.html#f:49"><span class="id" title="variable">f</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#4806e03a8439f8521169dfc83e768cdb"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#4806e03a8439f8521169dfc83e768cdb"><span class="id" title="notation">o</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:50"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f:49"><span class="id" title="variable">f</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#g:50"><span class="id" title="variable">g</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">H</span>.<br/>
<span class="id" title="tactic">specialize</span> (<span class="id" title="var">H</span> 1) <span class="id" title="keyword">as</span> (<span class="id" title="var">c__ino</span>&<span class="id" title="var">H</span>).<br/>
<span class="id" title="tactic">exists</span> 1,<span class="id" title="var">c__ino</span>. <span class="id" title="tactic">intros</span> ? ?%<span class="id" title="var">H</span>. <span class="id" title="var">lia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
</div>
<div class="doc">
<a id="lab11"></a><h2 class="section">O(poly)</h2>
</div>
<div class="code">
<br/>
<span class="id" title="keyword">Definition</span> <a id="inOPoly" class="idref" href="#inOPoly"><span class="id" title="definition">inOPoly</span></a> (<a id="f:51" class="idref" href="#f:51"><span class="id" title="binder">f</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <span class="id" title="keyword">Prop</span> :=<br/>
<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">exists</span></a> <a id="n:52" class="idref" href="#n:52"><span class="id" title="binder">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f:51"><span class="id" title="variable">f</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">∈</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">O</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">fun</span> <a id="x:53" class="idref" href="#x:53"><span class="id" title="binder">x</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#x:53"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#n:52"><span class="id" title="variable">n</span></a><a class="idref" href="Complexity.Complexity.ONotation.html#fb13635db5891cd876d35f6ab833523d"><span class="id" title="notation">)</span></a>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inOPoly_c" class="idref" href="#inOPoly_c"><span class="id" title="lemma">inOPoly_c</span></a> <a id="c:54" class="idref" href="#c:54"><span class="id" title="binder">c</span></a>: <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> => <a class="idref" href="Complexity.Complexity.ONotation.html#c:54"><span class="id" title="variable">c</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">exists</span> 1. <span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_c"><span class="id" title="lemma">inO_c</span></a>. <span class="id" title="var">cbn</span>. <span class="id" title="tactic">eapply</span> (<a class="idref" href="Complexity.Complexity.ONotation.html#inO_leq"><span class="id" title="lemma">inO_leq</span></a> (<span class="id" title="var">n0</span>:=1)). <span class="id" title="tactic">intros</span>. <span class="id" title="var">lia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inOPoly_x" class="idref" href="#inOPoly_x"><span class="id" title="lemma">inOPoly_x</span></a>: <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> (<span class="id" title="keyword">fun</span> <a id="x:55" class="idref" href="#x:55"><span class="id" title="binder">x</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#x:55"><span class="id" title="variable">x</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">exists</span> 1. <span class="id" title="var">cbn</span>. <span class="id" title="tactic">eapply</span> (<a class="idref" href="Complexity.Complexity.ONotation.html#inO_leq"><span class="id" title="lemma">inO_leq</span></a> (<span class="id" title="var">n0</span>:=1)). <span class="id" title="tactic">intros</span>. <span class="id" title="var">lia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inOPoly_add" class="idref" href="#inOPoly_add"><span class="id" title="lemma">inOPoly_add</span></a> <a id="f1:56" class="idref" href="#f1:56"><span class="id" title="binder">f1</span></a> <a id="f2:57" class="idref" href="#f2:57"><span class="id" title="binder">f2</span></a>: <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f1:56"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f2:57"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> (<span class="id" title="keyword">fun</span> <a id="x:58" class="idref" href="#x:58"><span class="id" title="binder">x</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#f1:56"><span class="id" title="variable">f1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#x:58"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f2:57"><span class="id" title="variable">f2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#x:58"><span class="id" title="variable">x</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> (<span class="id" title="var">n1</span>&?) (<span class="id" title="var">n2</span>&?).<br/>
<span class="id" title="tactic">exists</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Nat.html#max"><span class="id" title="definition">max</span></a> <span class="id" title="var">n1</span> <span class="id" title="var">n2</span>).<br/>
<span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_add_l"><span class="id" title="lemma">inO_add_l</span></a>.<br/>
<span class="id" title="var">all</span>:<span class="id" title="var">etransitivity</span>;[<span class="id" title="var">eassumption</span>|].<br/>
<span class="id" title="var">all</span>:<span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_leq"><span class="id" title="lemma">inO_leq</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">n0</span>:=1).<br/>
<span class="id" title="var">all</span>:<span class="id" title="tactic">intros</span> ? ?.<br/>
<span class="id" title="var">all</span>:<span class="id" title="tactic">eapply</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.pow_le_mono_r"><span class="id" title="lemma">Nat.pow_le_mono_r</span></a>. <span class="id" title="var">all</span>:<span class="id" title="var">Lia.nia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inOPoly_mul" class="idref" href="#inOPoly_mul"><span class="id" title="lemma">inOPoly_mul</span></a> <a id="f1:59" class="idref" href="#f1:59"><span class="id" title="binder">f1</span></a> <a id="f2:60" class="idref" href="#f2:60"><span class="id" title="binder">f2</span></a>: <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f1:59"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f2:60"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> (<span class="id" title="keyword">fun</span> <a id="x:61" class="idref" href="#x:61"><span class="id" title="binder">x</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#f1:59"><span class="id" title="variable">f1</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#x:61"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f2:60"><span class="id" title="variable">f2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#x:61"><span class="id" title="variable">x</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> (<span class="id" title="var">n1</span>&?) (<span class="id" title="var">n2</span>&?).<br/>
<span class="id" title="tactic">exists</span> (<span class="id" title="var">n1</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a><span class="id" title="var">n2</span>).<br/>
<span class="id" title="tactic">transitivity</span> (<span class="id" title="keyword">fun</span> <a id="x:63" class="idref" href="#x:63"><span class="id" title="binder">x</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#x:62"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <span class="id" title="var">n1</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#x:62"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a><span class="id" title="var">n2</span>).<br/>
1:<span class="id" title="var">now</span> <span class="id" title="tactic">eauto</span> <span class="id" title="keyword">using</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_mul_l"><span class="id" title="lemma">inO_mul_l</span></a>.<br/>
<span class="id" title="var">all</span>:<span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_leq"><span class="id" title="lemma">inO_leq</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">n0</span>:=0).<br/>
<span class="id" title="var">all</span>:<span class="id" title="tactic">intros</span> ? <span class="id" title="var">_</span>.<br/>
<span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.pow_add_r"><span class="id" title="lemma">Nat.pow_add_r</span></a>. <span class="id" title="var">Lia.nia</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inOPoly_pow" class="idref" href="#inOPoly_pow"><span class="id" title="lemma">inOPoly_pow</span></a> <a id="f:64" class="idref" href="#f:64"><span class="id" title="binder">f</span></a> <a id="c:65" class="idref" href="#c:65"><span class="id" title="binder">c</span></a>: <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f:64"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> (<span class="id" title="keyword">fun</span> <a id="x:66" class="idref" href="#x:66"><span class="id" title="binder">x</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#f:64"><span class="id" title="variable">f</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#x:66"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#c:65"><span class="id" title="variable">c</span></a>).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> (<span class="id" title="var">n</span>&<span class="id" title="var">H</span>). <span class="id" title="tactic">exists</span> (<span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">*</span></a><span class="id" title="var">c</span>).<br/>
<span class="id" title="tactic">destruct</span> <span class="id" title="var">H</span> <span class="id" title="keyword">as</span> (<span class="id" title="var">n0</span> & <span class="id" title="var">n1</span>&<span class="id" title="var">H</span>).<br/>
<span class="id" title="tactic">eexists</span> <span class="id" title="var">_</span>, <span class="id" title="var">n1</span>.<br/>
<span class="id" title="tactic">intros</span> ? <span class="id" title="var">H'</span>%<span class="id" title="var">H</span>. <span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.pow_le_mono_l"><span class="id" title="lemma">Nat.pow_le_mono_l</span></a>. 2:<span class="id" title="var">eassumption</span>.<br/>
<span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.pow_mul_l"><span class="id" title="lemma">Nat.pow_mul_l</span></a>,<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.pow_mul_r"><span class="id" title="lemma">Nat.pow_mul_r</span></a>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inOPoly_S" class="idref" href="#inOPoly_S"><span class="id" title="lemma">inOPoly_S</span></a> <a id="f:67" class="idref" href="#f:67"><span class="id" title="binder">f</span></a> : <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f:67"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> (<span class="id" title="keyword">fun</span> <a id="x:68" class="idref" href="#x:68"><span class="id" title="binder">x</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> (<a class="idref" href="Complexity.Complexity.ONotation.html#f:67"><span class="id" title="variable">f</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#x:68"><span class="id" title="variable">x</span></a>)).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">H</span>. <span class="id" title="tactic">eapply</span> (@<a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly_add"><span class="id" title="lemma">inOPoly_add</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> => 1) <span class="id" title="var">f</span>). 2: <span class="id" title="tactic">apply</span> <span class="id" title="var">H</span>.<br/>
<span class="id" title="tactic">apply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly_c"><span class="id" title="lemma">inOPoly_c</span></a>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Lemma</span> <a id="inOPoly_comp" class="idref" href="#inOPoly_comp"><span class="id" title="lemma">inOPoly_comp</span></a> <a id="f1:69" class="idref" href="#f1:69"><span class="id" title="binder">f1</span></a> <a id="f2:70" class="idref" href="#f2:70"><span class="id" title="binder">f2</span></a>: <a class="idref" href="Complexity.Complexity.Monotonic.html#monotonic"><span class="id" title="definition">monotonic</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f1:69"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f1:69"><span class="id" title="variable">f1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#f2:70"><span class="id" title="variable">f2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a> (<span class="id" title="keyword">fun</span> <a id="x:71" class="idref" href="#x:71"><span class="id" title="binder">x</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#f1:69"><span class="id" title="variable">f1</span></a> (<a class="idref" href="Complexity.Complexity.ONotation.html#f2:70"><span class="id" title="variable">f2</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#x:71"><span class="id" title="variable">x</span></a>)).<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> ? (<span class="id" title="var">n1</span>&?) (<span class="id" title="var">n2</span>&?).<br/>
<span class="id" title="tactic">exists</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Nat.html#max"><span class="id" title="definition">max</span></a> 1 <span class="id" title="var">n2</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">)*</span></a><span class="id" title="var">n1</span>).<br/>
<span class="id" title="var">etransitivity</span>.<br/>
{<span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_comp_l"><span class="id" title="lemma">inO_comp_l</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">g2</span>:=(<span class="id" title="keyword">fun</span> <a id="x:73" class="idref" href="#x:73"><span class="id" title="binder">x</span></a> => <a class="idref" href="Complexity.Complexity.ONotation.html#x:72"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Nat.html#max"><span class="id" title="definition">max</span></a> 1 <span class="id" title="var">n2</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">)</span></a>)).<br/>
1,3:<span class="id" title="var">eassumption</span>.<br/>
-<span class="id" title="tactic">rewrite</span> <span class="id" title="var">H1</span>. <span class="id" title="tactic">apply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_leq"><span class="id" title="lemma">inO_leq</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">n0</span>:=1). <span class="id" title="tactic">intros</span>.<br/>
<span class="id" title="tactic">eapply</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.pow_le_mono"><span class="id" title="lemma">Nat.pow_le_mono</span></a>;<span class="id" title="var">lia</span>.<br/>
-<span class="id" title="tactic">intros</span>. <span class="id" title="tactic">replace</span> <span class="id" title="var">x</span> <span class="id" title="keyword">with</span> (<span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a>1) <span class="id" title="tactic">at</span> 1 <span class="id" title="tactic">by</span> (<span class="id" title="var">cbn</span>;<span class="id" title="var">Lia.nia</span>).<br/>
<span class="id" title="var">decide</span> (<span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a>0). 2:<span class="id" title="var">now</span> <span class="id" title="tactic">eapply</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.pow_le_mono"><span class="id" title="lemma">Nat.pow_le_mono</span></a>;<span class="id" title="var">Lia.nia</span>.<br/>
<span class="id" title="tactic">subst</span> <span class="id" title="var">x</span>. <span class="id" title="tactic">rewrite</span> !<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.pow_0_l"><span class="id" title="lemma">Nat.pow_0_l</span></a>. <span class="id" title="var">all</span>:<span class="id" title="var">Lia.nia</span>.<br/>
-<span class="id" title="var">cbn</span> <span class="id" title="keyword">beta</span>. <span class="id" title="tactic">intros</span> <span class="id" title="var">c</span>.<br/>
<span class="id" title="tactic">exists</span> (<span class="id" title="var">c</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a><span class="id" title="var">n1</span>),0. <span class="id" title="tactic">intros</span>.<br/>
<span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.pow_mul_l"><span class="id" title="lemma">Nat.pow_mul_l</span></a>. <span class="id" title="tactic">reflexivity</span>.<br/>
}<br/>
<span class="id" title="var">cbn</span> <span class="id" title="keyword">beta</span>.<br/>
<span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inO_leq"><span class="id" title="lemma">inO_leq</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">n0</span>:=0). <span class="id" title="tactic">intros</span>.<br/>
<span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Arith.PeanoNat.html#Nat.pow_mul_r"><span class="id" title="lemma">Nat.pow_mul_r</span></a>. <span class="id" title="tactic">reflexivity</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="var">Smpl</span> <span class="id" title="keyword">Add</span> 10 (<span class="id" title="tactic">first</span> [ <span class="id" title="tactic">simple</span> <span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly_add"><span class="id" title="lemma">inOPoly_add</span></a> | <span class="id" title="tactic">simple</span> <span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly_S"><span class="id" title="lemma">inOPoly_S</span></a> | <span class="id" title="tactic">simple</span> <span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly_mul"><span class="id" title="lemma">inOPoly_mul</span></a> | <span class="id" title="tactic">simple</span> <span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly_c"><span class="id" title="lemma">inOPoly_c</span></a> | <span class="id" title="tactic">simple</span> <span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly_pow"><span class="id" title="lemma">inOPoly_pow</span></a> | <span class="id" title="tactic">simple</span> <span class="id" title="tactic">eapply</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly_x"><span class="id" title="lemma">inOPoly_x</span></a> | <span class="id" title="var">eassumption</span>]) : <span class="id" title="var">inO</span>.<br/>
<br/>
<span class="id" title="keyword">Instance</span> <a id="inO_inOPoly_trans" class="idref" href="#inO_inOPoly_trans"><span class="id" title="instance">inO_inOPoly_trans</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#Proper"><span class="id" title="class">Proper</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Program.Basics.html#flip"><span class="id" title="definition">Basics.flip</span></a> <a class="idref" href="Complexity.Complexity.ONotation.html#inO"><span class="id" title="definition">inO</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">==></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Program.Basics.html#impl"><span class="id" title="definition">Basics.impl</span></a>) <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">intros</span> ? ? ? [? <span class="id" title="var">R2</span>]. <span class="id" title="tactic">unfold</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a>. <span class="id" title="tactic">eexists</span>. <span class="id" title="tactic">setoid_rewrite</span> <- <span class="id" title="var">R2</span>. <span class="id" title="var">easy</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Instance</span> <a id="inOPoly_pointwise_leq" class="idref" href="#inOPoly_pointwise_leq"><span class="id" title="instance">inOPoly_pointwise_leq</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#Proper"><span class="id" title="class">Proper</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Program.Basics.html#flip"><span class="id" title="definition">Basics.flip</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#pointwise_relation"><span class="id" title="definition">pointwise_relation</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Peano.html#le"><span class="id" title="inductive">le</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">==></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Program.Basics.html#impl"><span class="id" title="definition">Basics.impl</span></a>) <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">unfold</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a>.<br/>
<span class="id" title="tactic">intros</span> ? ? <span class="id" title="var">R1</span>. <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> |-*. <span class="id" title="tactic">setoid_rewrite</span> <span class="id" title="var">R1</span>. <span class="id" title="var">easy</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
<br/>
<span class="id" title="keyword">Instance</span> <a id="inOPoly_pointwise_eq" class="idref" href="#inOPoly_pointwise_eq"><span class="id" title="instance">inOPoly_pointwise_eq</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#Proper"><span class="id" title="class">Proper</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#pointwise_relation"><span class="id" title="definition">pointwise_relation</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#eq"><span class="id" title="inductive">eq</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Classes.Morphisms.html#8dc5652698a6e16f72dd37bd17d3b973"><span class="id" title="notation">==></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#iff"><span class="id" title="definition">iff</span></a>) <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
<span class="id" title="tactic">unfold</span> <a class="idref" href="Complexity.Complexity.ONotation.html#inOPoly"><span class="id" title="definition">inOPoly</span></a>. <span class="id" title="tactic">intros</span> ? ? <span class="id" title="var">R1</span>. <span class="id" title="tactic">hnf</span>. <span class="id" title="tactic">setoid_rewrite</span> <span class="id" title="var">R1</span>. <span class="id" title="var">easy</span>.<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>
<div id="footer">
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
</div>
</div>
</body>
</html>
