diff options
Diffstat (limited to 'mathcomp/algebra')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 6dbfaf7..f7b2e0f 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -5619,6 +5619,7 @@ Ltac mexact x := by mapply x. Local Notation min := minr. Local Notation max := maxr. +Lemma minrC : @commutative R R min. Proof. mexact @minC. Qed. Lemma minrr : @idempotent R min. Proof. mexact @minxx. Qed. Lemma minr_l x y : x <= y -> min x y = x. Proof. mexact @min_l. Qed. Lemma minr_r x y : y <= x -> min x y = y. Proof. mexact @min_r. Qed. |