Skip to content

Instantly share code, notes, and snippets.

@vlj
Created February 19, 2020 20:05
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save vlj/408daf59ab39c4efae8e66658692dde0 to your computer and use it in GitHub Desktop.
Save vlj/408daf59ab39c4efae8e66658692dde0 to your computer and use it in GitHub Desktop.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice path.
From mathcomp Require Import div fintype tuple finfun bigop finset fingroup perm.
From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg ssrnum.
From mathcomp Require Import ssrint matrix order ssrint order.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Import GRing.Theory.
Import Num.Theory.
Import Order.Theory.
Lemma tmp00 (n m:nat):
n./2%:Z <= max n./2 m./2.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment