fact: CoInductive compare_T2 m n : bool -> bool -> bool -> Set := | CompareT2Lt of m < n : compare_T2 m n true false false | CompareT2Gt of m > n : compare_T2 m n false true false | CompareT2Eq of m = n : compare_T2 m n false false true.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)