Module mathcomp.classical.mathcomp_extra
From HB Require Import structures.From mathcomp Require Import boot order finmap algebra.
# MathComp extra
This files contains lemmas and definitions recently added in mathcomp,
in order to be able to compile analysis with older versions of mathcomp.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope ring_scope.
MathComp 2.7 additions