Merge pull request #490 from pi8027/fix-fin-dual-order

Add dual_finLatticeType and fix dual_finDistrLatticeType

1 files changed, 6 insertions, 1 deletions

diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 38ee13d..90ddfcb 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -3549,6 +3549,10 @@ Lemma botEdual : (dual_bottom : L^d) = 1 :> L. Proof. by []. Qed.
 Lemma topEdual : (dual_top : L^d) = 0 :> L. Proof. by []. Qed.
 
 End DualTBLattice.
+
+Canonical dual_finLatticeType d (T : finLatticeType d) :=
+  [finLatticeType of T^d].
+
 End DualTBLattice.
 
 Module Import TBLatticeTheory.
@@ -3682,11 +3686,12 @@ Context {L : tbDistrLatticeType}.
 Canonical dual_bDistrLatticeType := [bDistrLatticeType of L^d].
 Canonical dual_tbDistrLatticeType := [tbDistrLatticeType of L^d].
 
+End DualTBDistrLattice.
+
 Canonical dual_finDistrLatticeType d (T : finDistrLatticeType d) :=
   [finDistrLatticeType of T^d].
 
 End DualTBDistrLattice.
-End DualTBDistrLattice.
 
 Module Import TBDistrLatticeTheory.
 Section TBDistrLatticeTheory.