diff options
| author | Enrico Tassi | 2019-05-22 13:43:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-22 15:34:14 +0200 |
| commit | 748d716efb2f2f75946c8386e441ce1789806a39 (patch) | |
| tree | fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.algebra.fraction.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/mathcomp.algebra.fraction.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.algebra.fraction.html | 187 |
1 files changed, 93 insertions, 94 deletions
diff --git a/docs/htmldoc/mathcomp.algebra.fraction.html b/docs/htmldoc/mathcomp.algebra.fraction.html index 2b78b50..745fa06 100644 --- a/docs/htmldoc/mathcomp.algebra.fraction.html +++ b/docs/htmldoc/mathcomp.algebra.fraction.html @@ -21,7 +21,6 @@ <div class="code"> <span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> Distributed under the terms of CeCILL-B. *)</span><br/> -<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> <br/> </div> @@ -58,58 +57,58 @@ ratios are pairs of R, such that the second member is nonzero </div> <div class="code"> -<span class="id" title="keyword">Inductive</span> <a name="ratio"><span class="id" title="record">ratio</span></a> := <a name="mkRatio"><span class="id" title="constructor">mkRatio</span></a> { <a name="frac"><span class="id" title="projection">frac</span></a> :> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="method">frac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 }.<br/> -<span class="id" title="keyword">Definition</span> <a name="ratio_of"><span class="id" title="definition">ratio_of</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a>.<br/> +<span class="id" title="keyword">Inductive</span> <a name="ratio"><span class="id" title="record">ratio</span></a> := <a name="mkRatio"><span class="id" title="constructor">mkRatio</span></a> { <a name="frac"><span class="id" title="projection">frac</span></a> :> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="method">frac</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 }.<br/> +<span class="id" title="keyword">Definition</span> <a name="ratio_of"><span class="id" title="definition">ratio_of</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a>.<br/> <br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="projection">frac</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_of_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#6645671e2203a23d135a621a3cf0157c"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="ratio_EqMixin"><span class="id" title="definition">ratio_EqMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation"><:]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="projection">frac</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_of_subType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#aa8c179e7d847b79500c7558a661edb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#aa8c179e7d847b79500c7558a661edb0"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#aa8c179e7d847b79500c7558a661edb0"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#aa8c179e7d847b79500c7558a661edb0"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="ratio_EqMixin"><span class="id" title="definition">ratio_EqMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation"><:]</span></a>.<br/> <span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_eqType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio_EqMixin"><span class="id" title="definition">ratio_EqMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_of_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="ratio_ChoiceMixin"><span class="id" title="definition">ratio_ChoiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation"><:]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_of_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="ratio_ChoiceMixin"><span class="id" title="definition">ratio_ChoiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation"><:]</span></a>.<br/> <span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio_ChoiceMixin"><span class="id" title="definition">ratio_ChoiceMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_of_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ratio_of_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">]</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="denom_ratioP"><span class="id" title="lemma">denom_ratioP</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a>, <a class="idref" href="mathcomp.algebra.fraction.html#f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0. <br/> +<span class="id" title="keyword">Lemma</span> <a name="denom_ratioP"><span class="id" title="lemma">denom_ratioP</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a>, <a class="idref" href="mathcomp.algebra.fraction.html#f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0. <br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="ratio0"><span class="id" title="definition">ratio0</span></a> := (@<a class="idref" href="mathcomp.algebra.fraction.html#mkRatio"><span class="id" title="constructor">mkRatio</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a>0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Theory.oner_neq0"><span class="id" title="definition">oner_neq0</span></a> <span class="id" title="var">_</span>)).<br/> -<span class="id" title="keyword">Definition</span> <a name="Ratio"><span class="id" title="definition">Ratio</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">}</span></a> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#insubd"><span class="id" title="definition">insubd</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="ratio0"><span class="id" title="definition">ratio0</span></a> := (@<a class="idref" href="mathcomp.algebra.fraction.html#mkRatio"><span class="id" title="constructor">mkRatio</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Theory.oner_neq0"><span class="id" title="definition">oner_neq0</span></a> <span class="id" title="var">_</span>)).<br/> +<span class="id" title="keyword">Definition</span> <a name="Ratio"><span class="id" title="definition">Ratio</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">}</span></a> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#insubd"><span class="id" title="definition">insubd</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="numer_Ratio"><span class="id" title="lemma">numer_Ratio</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">).1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="numer_Ratio"><span class="id" title="lemma">numer_Ratio</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">).1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="denom_Ratio"><span class="id" title="lemma">denom_Ratio</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">).2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="denom_Ratio"><span class="id" title="lemma">denom_Ratio</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">).2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="numden_Ratio"><span class="id" title="definition">numden_Ratio</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#numer_Ratio"><span class="id" title="lemma">numer_Ratio</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#denom_Ratio"><span class="id" title="lemma">denom_Ratio</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="numden_Ratio"><span class="id" title="definition">numden_Ratio</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#numer_Ratio"><span class="id" title="lemma">numer_Ratio</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#denom_Ratio"><span class="id" title="lemma">denom_Ratio</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/> <br/> -<span class="id" title="keyword">CoInductive</span> <a name="Ratio_spec"><span class="id" title="inductive">Ratio_spec</span></a> (<span class="id" title="var">n</span> <span class="id" title="var">d</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#2f9285fe1a1256233574a22b02c18c89"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span> :=<br/> - | <a name="RatioNull"><span class="id" title="constructor">RatioNull</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0 : <a class="idref" href="mathcomp.algebra.fraction.html#Ratio_spec"><span class="id" title="inductive">Ratio_spec</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> 0<br/> - | <a name="RatioNonNull"><span class="id" title="constructor">RatioNonNull</span></a> (<span class="id" title="var">d_neq0</span> : <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0) : <br/> - <a class="idref" href="mathcomp.algebra.fraction.html#Ratio_spec"><span class="id" title="inductive">Ratio_spec</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> (@<a class="idref" href="mathcomp.algebra.fraction.html#mkRatio"><span class="id" title="constructor">mkRatio</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d_neq0"><span class="id" title="variable">d_neq0</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a>.<br/> +<span class="id" title="keyword">Variant</span> <a name="Ratio_spec"><span class="id" title="inductive">Ratio_spec</span></a> (<span class="id" title="var">n</span> <span class="id" title="var">d</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#50c2e3815a42123311bc4308989023fc"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Type</span> :=<br/> + | <a name="RatioNull"><span class="id" title="constructor">RatioNull</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0 : <a class="idref" href="mathcomp.algebra.fraction.html#Ratio_spec"><span class="id" title="inductive">Ratio_spec</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> 0<br/> + | <a name="RatioNonNull"><span class="id" title="constructor">RatioNonNull</span></a> (<span class="id" title="var">d_neq0</span> : <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0) : <br/> + <a class="idref" href="mathcomp.algebra.fraction.html#Ratio_spec"><span class="id" title="inductive">Ratio_spec</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> (@<a class="idref" href="mathcomp.algebra.fraction.html#mkRatio"><span class="id" title="constructor">mkRatio</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d_neq0"><span class="id" title="variable">d_neq0</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a>.<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="RatioP"><span class="id" title="lemma">RatioP</span></a> <span class="id" title="var">n</span> <span class="id" title="var">d</span> : <a class="idref" href="mathcomp.algebra.fraction.html#Ratio_spec"><span class="id" title="inductive">Ratio_spec</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a> (<a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#d"><span class="id" title="variable">d</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="Ratio0"><span class="id" title="lemma">Ratio0</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="Ratio0"><span class="id" title="lemma">Ratio0</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.fraction.html#FracDomain"><span class="id" title="section">FracDomain</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="d415e1de9145ec99991d83aeed2ffede"><span class="id" title="notation">"</span></a>{ 'ratio' T }" := (<a class="idref" href="mathcomp.algebra.fraction.html#ratio_of"><span class="id" title="definition">ratio_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="03823952a2553ec6b46621aa2d9ce68e"><span class="id" title="notation">"</span></a>{ 'ratio' T }" := (<a class="idref" href="mathcomp.algebra.fraction.html#ratio_of"><span class="id" title="definition">ratio_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)).<br/> <span class="id" title="keyword">Identity</span> <span class="id" title="keyword">Coercion</span> <span class="id" title="var">type_fracdomain_of</span> : <span class="id" title="var">ratio_of</span> >-> <span class="id" title="var">ratio</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">"</span></a>'\n_' x" := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="projection">frac</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">).1</span></a><br/> +<span class="id" title="keyword">Notation</span> <a name="14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">"</span></a>'\n_' x" := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="projection">frac</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">).1</span></a><br/> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "'\n_' x").<br/> -<span class="id" title="keyword">Notation</span> <a name="78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">"</span></a>'\d_' x" := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="projection">frac</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">).2</span></a><br/> +<span class="id" title="keyword">Notation</span> <a name="e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">"</span></a>'\d_' x" := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#frac"><span class="id" title="projection">frac</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">).2</span></a><br/> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "'\d_' x").<br/> <br/> @@ -134,16 +133,16 @@ <span class="id" title="keyword">Definition</span> <a name="FracField.equivf"><span class="id" title="definition">equivf</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> := <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf_notation"><span class="id" title="abbreviation">equivf_notation</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.equivfE"><span class="id" title="lemma">equivfE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf_notation"><span class="id" title="abbreviation">equivf_notation</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.equivfE"><span class="id" title="lemma">equivfE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf_notation"><span class="id" title="abbreviation">equivf_notation</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_refl"><span class="id" title="lemma">equivf_refl</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflexive"><span class="id" title="definition">reflexive</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_refl"><span class="id" title="lemma">equivf_refl</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflexive"><span class="id" title="definition">reflexive</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_sym"><span class="id" title="lemma">equivf_sym</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#symmetric"><span class="id" title="definition">symmetric</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_sym"><span class="id" title="lemma">equivf_sym</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#symmetric"><span class="id" title="definition">symmetric</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_trans"><span class="id" title="lemma">equivf_trans</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#transitive"><span class="id" title="definition">transitive</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_trans"><span class="id" title="lemma">equivf_trans</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#transitive"><span class="id" title="definition">transitive</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a>.<br/> <br/> </div> @@ -155,9 +154,9 @@ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">equivf_equiv</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#EquivRel"><span class="id" title="abbreviation">EquivRel</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf_refl"><span class="id" title="lemma">equivf_refl</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf_sym"><span class="id" title="lemma">equivf_sym</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf_trans"><span class="id" title="lemma">equivf_trans</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="FracField.type"><span class="id" title="definition">type</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">eq_quot</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#73f0d3e79bf803b4c740bbb9fa38aa76"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="FracField.type_of"><span class="id" title="definition">type_of</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">"</span></a>{ 'fraction' T }" := (<a class="idref" href="mathcomp.algebra.fraction.html#FracField.type_of"><span class="id" title="definition">type_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)).<br/> +<span class="id" title="keyword">Definition</span> <a name="FracField.type"><span class="id" title="definition">type</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">eq_quot</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#0dc587318a1236d89082bca629a5db9b"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FracField.type_of"><span class="id" title="definition">type_of</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a name="563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">"</span></a>{ 'fraction' T }" := (<a class="idref" href="mathcomp.algebra.fraction.html#FracField.type_of"><span class="id" title="definition">type_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)).<br/> <br/> </div> @@ -166,16 +165,16 @@ we recover some structure for the quotient </div> <div class="code"> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_quotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_eqType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_eqQuotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">eqQuotType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_quotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_eqType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_eqQuotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><span class="id" title="notation">eqQuotType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><span class="id" title="notation">]</span></a>.<br/> <br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_quotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_eqType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_eqQuotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">eqQuotType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#b7a0622a915c3e5a7396a3208b40639a"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_quotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_eqType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_choiceType</span> := <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_eqQuotType</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><span class="id" title="notation">eqQuotType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#dc3d569865bd181e003ea2b17400befd"><span class="id" title="notation">]</span></a>.<br/> <br/> </div> @@ -184,72 +183,72 @@ we explain what was the equivalence on the quotient </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_def"><span class="id" title="lemma">equivf_def</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#433801266bfe38f0ebd6037860203596"><span class="id" title="notation">]</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_def"><span class="id" title="lemma">equivf_def</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#ratio"><span class="id" title="record">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a>) : <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#e3392789fbfaf247c0fb823980d6e8ff"><span class="id" title="notation">]</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_r"><span class="id" title="lemma">equivf_r</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_r"><span class="id" title="lemma">equivf_r</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">pi_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">pi_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">)</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_l"><span class="id" title="lemma">equivf_l</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#997e4486c98ae8c7d206ef25b33fb606"><span class="id" title="notation">pi_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.equivf_l"><span class="id" title="lemma">equivf_l</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">pi_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#repr"><span class="id" title="abbreviation">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3337bf2cd4a8dc684c396fc9814b46a9"><span class="id" title="notation">pi_type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.numer0"><span class="id" title="lemma">numer0</span></a> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">mod_eq</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#ec726891ee056b01e6c94482e2a4af00"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.numer0"><span class="id" title="lemma">numer0</span></a> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#ratio0"><span class="id" title="definition">ratio0</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">mod_eq</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.equivf"><span class="id" title="definition">equivf</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#3799fc59ee103320fa3882288df6a9c4"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.Ratio_numden"><span class="id" title="lemma">Ratio_numden</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.Ratio_numden"><span class="id" title="lemma">Ratio_numden</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="FracField.tofrac"><span class="id" title="definition">tofrac</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_embed"><span class="id" title="abbreviation">lift_embed</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a> ⇒ <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> 1).<br/> +<span class="id" title="keyword">Definition</span> <a name="FracField.tofrac"><span class="id" title="definition">tofrac</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_embed"><span class="id" title="abbreviation">lift_embed</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a> ⇒ <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> 1).<br/> <span class="id" title="keyword">Canonical</span> <span class="id" title="var">tofrac_pi_morph</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiEmbed"><span class="id" title="abbreviation">PiEmbed</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.tofrac"><span class="id" title="definition">tofrac</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">"</span></a>x %:F" := (@<a class="idref" href="mathcomp.algebra.fraction.html#FracField.tofrac"><span class="id" title="definition">tofrac</span></a> <span class="id" title="var">x</span>).<br/> +<span class="id" title="keyword">Notation</span> <a name="43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">"</span></a>x %:F" := (@<a class="idref" href="mathcomp.algebra.fraction.html#FracField.tofrac"><span class="id" title="definition">tofrac</span></a> <span class="id" title="var">x</span>).<br/> <br/> <span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> <span class="id" title="var">c</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="FracField.addf"><span class="id" title="definition">addf</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> (<a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a>) (<a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_y</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="FracField.add"><span class="id" title="definition">add</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_op2"><span class="id" title="abbreviation">lift_op2</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.addf"><span class="id" title="definition">addf</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FracField.addf"><span class="id" title="definition">addf</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> (<a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a>) (<a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_y</span></a>).<br/> +<span class="id" title="keyword">Definition</span> <a name="FracField.add"><span class="id" title="definition">add</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_op2"><span class="id" title="abbreviation">lift_op2</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.addf"><span class="id" title="definition">addf</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.pi_add"><span class="id" title="lemma">pi_add</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.addf"><span class="id" title="definition">addf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.pi_add"><span class="id" title="lemma">pi_add</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.addf"><span class="id" title="definition">addf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">}</span></a>.<br/> <span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_add_morph</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph2"><span class="id" title="abbreviation">PiMorph2</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.pi_add"><span class="id" title="lemma">pi_add</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="FracField.oppf"><span class="id" title="definition">oppf</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="FracField.opp"><span class="id" title="definition">opp</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_op1"><span class="id" title="abbreviation">lift_op1</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.oppf"><span class="id" title="definition">oppf</span></a>.<br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.pi_opp"><span class="id" title="lemma">pi_opp</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.oppf"><span class="id" title="definition">oppf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.opp"><span class="id" title="definition">opp</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FracField.oppf"><span class="id" title="definition">oppf</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#8d0566c961139ec21811f52ef0c317db"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FracField.opp"><span class="id" title="definition">opp</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_op1"><span class="id" title="abbreviation">lift_op1</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.oppf"><span class="id" title="definition">oppf</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.pi_opp"><span class="id" title="lemma">pi_opp</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.oppf"><span class="id" title="definition">oppf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.opp"><span class="id" title="definition">opp</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">}</span></a>.<br/> <span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_opp_morph</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph1"><span class="id" title="abbreviation">PiMorph1</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.pi_opp"><span class="id" title="lemma">pi_opp</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="FracField.mulf"><span class="id" title="definition">mulf</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> (<a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_y</span></a>) (<a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_y</span></a>).<br/> -<span class="id" title="keyword">Definition</span> <a name="FracField.mul"><span class="id" title="definition">mul</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_op2"><span class="id" title="abbreviation">lift_op2</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mulf"><span class="id" title="definition">mulf</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FracField.mulf"><span class="id" title="definition">mulf</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> (<a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_y</span></a>) (<a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_y</span></a>).<br/> +<span class="id" title="keyword">Definition</span> <a name="FracField.mul"><span class="id" title="definition">mul</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_op2"><span class="id" title="abbreviation">lift_op2</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mulf"><span class="id" title="definition">mulf</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.pi_mul"><span class="id" title="lemma">pi_mul</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mulf"><span class="id" title="definition">mulf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.pi_mul"><span class="id" title="lemma">pi_mul</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mulf"><span class="id" title="definition">mulf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">}</span></a>.<br/> <span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_mul_morph</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph2"><span class="id" title="abbreviation">PiMorph2</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.pi_mul"><span class="id" title="lemma">pi_mul</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="FracField.invf"><span class="id" title="definition">invf</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="FracField.inv"><span class="id" title="definition">inv</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_op1"><span class="id" title="abbreviation">lift_op1</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e36ff61a3bfee78c33cdeff909f4190f"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.invf"><span class="id" title="definition">invf</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FracField.invf"><span class="id" title="definition">invf</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.dom"><span class="id" title="abbreviation">dom</span></a> := <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FracField.inv"><span class="id" title="definition">inv</span></a> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#lift_op1"><span class="id" title="abbreviation">lift_op1</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.FracField.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#563ad5e6433eb405cbb9f8f75f49cdce"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.invf"><span class="id" title="definition">invf</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.pi_inv"><span class="id" title="lemma">pi_inv</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#f090f187f28139994197271ddc594c91"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.invf"><span class="id" title="definition">invf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.inv"><span class="id" title="definition">inv</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.pi_inv"><span class="id" title="lemma">pi_inv</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#c3fdc30b5d212c820acf98356210d6f7"><span class="id" title="notation">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.invf"><span class="id" title="definition">invf</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.inv"><span class="id" title="definition">inv</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">}</span></a>.<br/> <span class="id" title="keyword">Canonical</span> <span class="id" title="var">pi_inv_morph</span> := <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#PiMorph1"><span class="id" title="abbreviation">PiMorph1</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.pi_inv"><span class="id" title="lemma">pi_inv</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.addA"><span class="id" title="lemma">addA</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#associative"><span class="id" title="definition">associative</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.addA"><span class="id" title="lemma">addA</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#associative"><span class="id" title="definition">associative</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.addC"><span class="id" title="lemma">addC</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.addC"><span class="id" title="lemma">addC</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.add0_l"><span class="id" title="lemma">add0_l</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.add0_l"><span class="id" title="lemma">add0_l</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.addN_l"><span class="id" title="lemma">addN_l</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_inverse"><span class="id" title="definition">left_inverse</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.opp"><span class="id" title="definition">opp</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.addN_l"><span class="id" title="lemma">addN_l</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#left_inverse"><span class="id" title="definition">left_inverse</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.opp"><span class="id" title="definition">opp</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/> <br/> </div> @@ -262,19 +261,19 @@ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_zmodType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.ZmodType"><span class="id" title="abbreviation">ZmodType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.frac_zmodMixin"><span class="id" title="definition">frac_zmodMixin</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.mulA"><span class="id" title="lemma">mulA</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#associative"><span class="id" title="definition">associative</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.mulA"><span class="id" title="lemma">mulA</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#associative"><span class="id" title="definition">associative</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.mulC"><span class="id" title="lemma">mulC</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.mulC"><span class="id" title="lemma">mulC</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.mul1_l"><span class="id" title="lemma">mul1_l</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> 1<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.mul1_l"><span class="id" title="lemma">mul1_l</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> 1<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.mul_addl"><span class="id" title="lemma">mul_addl</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_distributive"><span class="id" title="definition">left_distributive</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.mul_addl"><span class="id" title="lemma">mul_addl</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#left_distributive"><span class="id" title="definition">left_distributive</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.add"><span class="id" title="definition">add</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.nonzero1"><span class="id" title="lemma">nonzero1</span></a> : 1<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#9e45f909d1732d6d9e153b650829bccf"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#9e45f909d1732d6d9e153b650829bccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.nonzero1"><span class="id" title="lemma">nonzero1</span></a> : 1<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#228e85e3c31a939cba019f255574c875"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#228e85e3c31a939cba019f255574c875"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a>.<br/> <br/> </div> @@ -288,10 +287,10 @@ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_comRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.ComRingType"><span class="id" title="abbreviation">ComRingType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mulC"><span class="id" title="lemma">mulC</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.mulV_l"><span class="id" title="lemma">mulV_l</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">a</span>, <a class="idref" href="mathcomp.algebra.fraction.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a> (<a class="idref" href="mathcomp.algebra.fraction.html#FracField.inv"><span class="id" title="definition">inv</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#a"><span class="id" title="variable">a</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.mulV_l"><span class="id" title="lemma">mulV_l</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">a</span>, <a class="idref" href="mathcomp.algebra.fraction.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mul"><span class="id" title="definition">mul</span></a> (<a class="idref" href="mathcomp.algebra.fraction.html#FracField.inv"><span class="id" title="definition">inv</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#a"><span class="id" title="variable">a</span></a>) <a class="idref" href="mathcomp.algebra.fraction.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="FracField.inv0"><span class="id" title="lemma">inv0</span></a> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.inv"><span class="id" title="definition">inv</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#0d67298a1649a05812baec7889fc3f77"><span class="id" title="notation">F</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FracField.inv0"><span class="id" title="lemma">inv0</span></a> : <a class="idref" href="mathcomp.algebra.fraction.html#FracField.inv"><span class="id" title="definition">inv</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0<a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#43ec65a9336417d9a06d4bf6447267e6"><span class="id" title="notation">F</span></a>.<br/> <br/> </div> @@ -302,7 +301,7 @@ <div class="code"> <span class="id" title="keyword">Definition</span> <a name="FracField.RatFieldUnitMixin"><span class="id" title="definition">RatFieldUnitMixin</span></a> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.FieldUnitMixin"><span class="id" title="abbreviation">FieldUnitMixin</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.mulV_l"><span class="id" title="lemma">mulV_l</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.inv0"><span class="id" title="lemma">inv0</span></a>.<br/> <span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_unitRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.UnitRing.Exports.UnitRingType"><span class="id" title="abbreviation">UnitRingType</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.RatFieldUnitMixin"><span class="id" title="definition">RatFieldUnitMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_comUnitRingType</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">comUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_comUnitRingType</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">comUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.type"><span class="id" title="definition">type</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">]</span></a>.<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="FracField.field_axiom"><span class="id" title="lemma">field_axiom</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.mixin_of"><span class="id" title="definition">GRing.Field.mixin_of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracField.frac_unitRingType"><span class="id" title="definition">frac_unitRingType</span></a>.<br/> @@ -324,9 +323,9 @@ <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.fraction.html#FracField"><span class="id" title="module">FracField</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">"</span></a>{ 'fraction' T }" := (<a class="idref" href="mathcomp.algebra.fraction.html#type_of"><span class="id" title="definition">FracField.type_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)).<br/> +<span class="id" title="keyword">Notation</span> <a name="3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">"</span></a>{ 'fraction' T }" := (<a class="idref" href="mathcomp.algebra.fraction.html#type_of"><span class="id" title="definition">FracField.type_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)).<br/> <span class="id" title="keyword">Notation</span> <a name="equivf"><span class="id" title="abbreviation">equivf</span></a> := (@<a class="idref" href="mathcomp.algebra.fraction.html#equivf"><span class="id" title="definition">FracField.equivf</span></a> <span class="id" title="var">_</span>).<br/> -<span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">denom_ratioP</span>.<br/> +<span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">denom_ratioP</span> : <span class="id" title="var">core</span>.<br/> <br/> <span class="id" title="keyword">Section</span> <a name="Canonicals"><span class="id" title="section">Canonicals</span></a>.<br/> @@ -352,16 +351,16 @@ <span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_idomainType</span>.<br/> <span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.frac_fieldType</span>.<br/> <span class="id" title="keyword">Canonical</span> <span class="id" title="var">FracField.tofrac_pi_morph</span>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_quotType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#a70f324fea4d80f55c2255a07c19c5c5"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#cb062fd562aed512787df99359c6e3f2"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#1731a28227324c9e5fc49499029635b3"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_zmodType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">zmodType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af6385fc2df84aeeec6855073f75cc68"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_ringType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">ringType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#dee4f3431027813095272c568fc6b5ce"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_comRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">comRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#57b384122345a94c564987d4b6ee9f0f"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_unitRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">unitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#f02859ca87d7563e473a6ba817bdc33f"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_comUnitRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">comUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#e3ee791c903b0283e51d52d0692558ec"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_idomainType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">idomainType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#9894f8fff6e44a40eb9fd9cfcbde7780"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_fieldType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">fieldType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#263b7369591a3bd7d72bcccade4f706e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#005edfce3bb0bbe988e3333ca30adc0f"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_quotType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">quotType</span></a> <a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.generic_quotient.html#2b6ecaeff71b4103d20b05dbc196dba6"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_zmodType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#97b11d2a158d9db11032c2626798c6ac"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#97b11d2a158d9db11032c2626798c6ac"><span class="id" title="notation">zmodType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#97b11d2a158d9db11032c2626798c6ac"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#97b11d2a158d9db11032c2626798c6ac"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_ringType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#964cf6dee45a836ccf0bcd3d85de1071"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#964cf6dee45a836ccf0bcd3d85de1071"><span class="id" title="notation">ringType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#964cf6dee45a836ccf0bcd3d85de1071"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#964cf6dee45a836ccf0bcd3d85de1071"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_comRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d"><span class="id" title="notation">comRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#8b92acac231ba6173223cf75164fca3d"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_unitRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e"><span class="id" title="notation">unitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2734494507570795a22f59746d1c0f0e"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_comUnitRingType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">comUnitRingType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2dfeb3fb2088b370ad93742d4f23a0dc"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_idomainType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de"><span class="id" title="notation">idomainType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b10128495340407de3c7b321ce0c78de"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">frac_of_fieldType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2"><span class="id" title="notation">fieldType</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">fraction</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#3462e6409a0337f179dbfc80d0a22070"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#be36f4c61e9a82f836d531a63f34e6c2"><span class="id" title="notation">]</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.fraction.html#Canonicals"><span class="id" title="section">Canonicals</span></a>.<br/> @@ -376,7 +375,7 @@ <span class="id" title="keyword">Variable</span> <a name="FracFieldTheory.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.idomainType"><span class="id" title="abbreviation">idomainType</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="Ratio_numden"><span class="id" title="lemma">Ratio_numden</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#d415e1de9145ec99991d83aeed2ffede"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d415e1de9145ec99991d83aeed2ffede"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracFieldTheory.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d415e1de9145ec99991d83aeed2ffede"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#f62bb085e3fcb9d2a4a79dd8d82a5940"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#78f4b9d167e42d91a549f3b4b842aac9"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="Ratio_numden"><span class="id" title="lemma">Ratio_numden</span></a> (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.fraction.html#03823952a2553ec6b46621aa2d9ce68e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.fraction.html#03823952a2553ec6b46621aa2d9ce68e"><span class="id" title="notation">ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#FracFieldTheory.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.fraction.html#03823952a2553ec6b46621aa2d9ce68e"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.algebra.fraction.html#Ratio"><span class="id" title="definition">Ratio</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#14ffbcbb027e0dd70b8653f98ff33b0b"><span class="id" title="notation">n_x</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.fraction.html#e48cc477c757cb023cbbc39a728576e3"><span class="id" title="notation">d_x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a>.<br/> <br/> </div> @@ -405,21 +404,21 @@ tests </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="tofrac0"><span class="id" title="lemma">tofrac0</span></a> : 0<a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0. <br/> -<span class="id" title="keyword">Lemma</span> <a name="tofracN"><span class="id" title="lemma">tofracN</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">}</span></a>. <br/> -<span class="id" title="keyword">Lemma</span> <a name="tofracD"><span class="id" title="lemma">tofracD</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">}</span></a>. <br/> -<span class="id" title="keyword">Lemma</span> <a name="tofracB"><span class="id" title="lemma">tofracB</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">}</span></a>. <br/> -<span class="id" title="keyword">Lemma</span> <a name="tofracMn"><span class="id" title="lemma">tofracMn</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#891e51846c7d1d63a9cb5458374cf308"><span class="id" title="notation">*+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">}</span></a>. <br/> -<span class="id" title="keyword">Lemma</span> <a name="tofracMNn"><span class="id" title="lemma">tofracMNn</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#3baee4193385688d2f1fcb170107cf5b"><span class="id" title="notation">*-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">}</span></a>. <br/> -<span class="id" title="keyword">Lemma</span> <a name="tofrac1"><span class="id" title="lemma">tofrac1</span></a> : 1<a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1. <br/> -<span class="id" title="keyword">Lemma</span> <a name="tofracM"><span class="id" title="lemma">tofracM</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">}</span></a>. <br/> -<span class="id" title="keyword">Lemma</span> <a name="tofracX"><span class="id" title="lemma">tofracX</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">}</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="tofrac0"><span class="id" title="lemma">tofrac0</span></a> : 0<a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0. <br/> +<span class="id" title="keyword">Lemma</span> <a name="tofracN"><span class="id" title="lemma">tofracN</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#8d0566c961139ec21811f52ef0c317db"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">}</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="tofracD"><span class="id" title="lemma">tofracD</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">}</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="tofracB"><span class="id" title="lemma">tofracB</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#51dc792c356ca1a71a3094b50d6bb2fb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">}</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="tofracMn"><span class="id" title="lemma">tofracMn</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#e9001f602764f7896bb1eb34bf606a23"><span class="id" title="notation">*+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">}</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="tofracMNn"><span class="id" title="lemma">tofracMNn</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#e4d9eba2da60fcfead1a1c78283587ed"><span class="id" title="notation">*-</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">}</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="tofrac1"><span class="id" title="lemma">tofrac1</span></a> : 1<a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">F</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1. <br/> +<span class="id" title="keyword">Lemma</span> <a name="tofracM"><span class="id" title="lemma">tofracM</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">}</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="tofracX"><span class="id" title="lemma">tofracX</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#tofrac"><span class="id" title="abbreviation">tofrac</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#663140372ac3b275aae871b74b140513"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#3d6621e6eef40dcc7dc9a612222d0b4e"><span class="id" title="notation">}</span></a>. <br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="tofrac_eq"><span class="id" title="lemma">tofrac_eq</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracFieldTheory.R"><span class="id" title="variable">R</span></a>): <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">F</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="tofrac_eq"><span class="id" title="lemma">tofrac_eq</span></a> (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracFieldTheory.R"><span class="id" title="variable">R</span></a>): <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">F</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.algebra.fraction.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="tofrac_eq0"><span class="id" title="lemma">tofrac_eq0</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracFieldTheory.R"><span class="id" title="variable">R</span></a>): <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d9d6d1f4f8cd2abb4d51f5ecc485c2ac"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="tofrac_eq0"><span class="id" title="lemma">tofrac_eq0</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.fraction.html#FracFieldTheory.R"><span class="id" title="variable">R</span></a>): <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.fraction.html#d0a54053fdb6fcdcd95f4ef121d7b80d"><span class="id" title="notation">F</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.fraction.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.fraction.html#FracFieldTheory"><span class="id" title="section">FracFieldTheory</span></a>.<br/> </div> </div> |