Deploying to gh-pages from @ 34f5009 🚀

master/Data.Nat.Properties.html

@@ -18,7 +18,7 @@
 <a id="638" class="Keyword">open</a> <a id="643" class="Keyword">import</a> <a id="650" href="Algebra.Definitions.RawMagma.html" class="Module">Algebra.Definitions.RawMagma</a> <a id="679" class="Keyword">using</a> <a id="685" class="Symbol">(</a><a id="686" href="Algebra.Definitions.RawMagma.html#1414" class="InductiveConstructor Operator">_,_</a><a id="689" class="Symbol">)</a>
 <a id="691" class="Keyword">open</a> <a id="696" class="Keyword">import</a> <a id="703" href="Algebra.Morphism.html" class="Module">Algebra.Morphism</a>
 <a id="720" class="Keyword">open</a> <a id="725" class="Keyword">import</a> <a id="732" href="Algebra.Consequences.Propositional.html" class="Module">Algebra.Consequences.Propositional</a>
-  <a id="769" class="Keyword">using</a> <a id="775" class="Symbol">(</a><a id="776" href="Algebra.Consequences.Setoid.html#13066" class="Function">comm+cancelˡ⇒cancelʳ</a><a id="796" class="Symbol">;</a> <a id="798" href="Algebra.Consequences.Propositional.html#3445" class="Function">comm∧distrʳ⇒distrˡ</a><a id="816" class="Symbol">;</a> <a id="818" href="Algebra.Consequences.Propositional.html#3305" class="Function">comm∧distrˡ⇒distrʳ</a><a id="836" class="Symbol">)</a>
+  <a id="769" class="Keyword">using</a> <a id="775" class="Symbol">(</a><a id="776" href="Algebra.Consequences.Setoid.html#3744" class="Function">comm∧cancelˡ⇒cancelʳ</a><a id="796" class="Symbol">;</a> <a id="798" href="Algebra.Consequences.Propositional.html#3445" class="Function">comm∧distrʳ⇒distrˡ</a><a id="816" class="Symbol">;</a> <a id="818" href="Algebra.Consequences.Propositional.html#3305" class="Function">comm∧distrˡ⇒distrʳ</a><a id="836" class="Symbol">)</a>
 <a id="838" class="Keyword">open</a> <a id="843" class="Keyword">import</a> <a id="850" href="Algebra.Construct.NaturalChoice.Base.html" class="Module">Algebra.Construct.NaturalChoice.Base</a>
   <a id="889" class="Keyword">using</a> <a id="895" class="Symbol">(</a><a id="896" href="Algebra.Construct.NaturalChoice.Base.html#990" class="Record">MinOperator</a><a id="907" class="Symbol">;</a> <a id="909" href="Algebra.Construct.NaturalChoice.Base.html#1191" class="Record">MaxOperator</a><a id="920" class="Symbol">)</a>
 <a id="922" class="Keyword">import</a> <a id="929" href="Algebra.Construct.NaturalChoice.MinMaxOp.html" class="Module">Algebra.Construct.NaturalChoice.MinMaxOp</a> <a id="970" class="Symbol">as</a> <a id="973" class="Module">MinMaxOp</a>
@@ -562,7 +562,7 @@
 <a id="15922" href="Data.Nat.Properties.html#15851" class="Function">+-cancelˡ-≡</a> <a id="15934" class="Symbol">(</a><a id="15935" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="15939" href="Data.Nat.Properties.html#15939" class="Bound">m</a><a id="15940" class="Symbol">)</a> <a id="15942" class="Symbol">_</a> <a id="15944" class="Symbol">_</a> <a id="15946" href="Data.Nat.Properties.html#15946" class="Bound">eq</a> <a id="15949" class="Symbol">=</a> <a id="15951" href="Data.Nat.Properties.html#15851" class="Function">+-cancelˡ-≡</a> <a id="15963" href="Data.Nat.Properties.html#15939" class="Bound">m</a> <a id="15965" class="Symbol">_</a> <a id="15967" class="Symbol">_</a> <a id="15969" class="Symbol">(</a><a id="15970" href="Relation.Binary.PropositionalEquality.Core.html#1339" class="Function">cong</a> <a id="15975" href="Data.Nat.Base.html#5272" class="Function">pred</a> <a id="15980" href="Data.Nat.Properties.html#15946" class="Bound">eq</a><a id="15982" class="Symbol">)</a>
 
 <a id="+-cancelʳ-≡"></a><a id="15985" href="Data.Nat.Properties.html#15985" class="Function">+-cancelʳ-≡</a> <a id="15997" class="Symbol">:</a> <a id="15999" href="Algebra.Definitions.html#4427" class="Function">RightCancellative</a> <a id="16017" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">_≡_</a> <a id="16021" href="Agda.Builtin.Nat.html#336" class="Primitive Operator">_+_</a>
-<a id="16025" href="Data.Nat.Properties.html#15985" class="Function">+-cancelʳ-≡</a> <a id="16037" class="Symbol">=</a> <a id="16039" href="Algebra.Consequences.Setoid.html#13066" class="Function">comm+cancelˡ⇒cancelʳ</a> <a id="16060" href="Data.Nat.Properties.html#15642" class="Function">+-comm</a> <a id="16067" href="Data.Nat.Properties.html#15851" class="Function">+-cancelˡ-≡</a>
+<a id="16025" href="Data.Nat.Properties.html#15985" class="Function">+-cancelʳ-≡</a> <a id="16037" class="Symbol">=</a> <a id="16039" href="Algebra.Consequences.Setoid.html#3744" class="Function">comm∧cancelˡ⇒cancelʳ</a> <a id="16060" href="Data.Nat.Properties.html#15642" class="Function">+-comm</a> <a id="16067" href="Data.Nat.Properties.html#15851" class="Function">+-cancelˡ-≡</a>
 
 <a id="+-cancel-≡"></a><a id="16080" href="Data.Nat.Properties.html#16080" class="Function">+-cancel-≡</a> <a id="16091" class="Symbol">:</a> <a id="16093" href="Algebra.Definitions.html#4522" class="Function">Cancellative</a> <a id="16106" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">_≡_</a> <a id="16110" href="Agda.Builtin.Nat.html#336" class="Primitive Operator">_+_</a>
 <a id="16114" href="Data.Nat.Properties.html#16080" class="Function">+-cancel-≡</a> <a id="16125" class="Symbol">=</a> <a id="16127" href="Data.Nat.Properties.html#15851" class="Function">+-cancelˡ-≡</a> <a id="16139" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="16141" href="Data.Nat.Properties.html#15985" class="Function">+-cancelʳ-≡</a>