fact: CoInductive compare_T3 m n : bool -> bool -> bool -> Set := | CompareT3Lt of m < n : compare_T3 m n true false false | CompareT3Gt of m > n : compare_T3 m n false true false | CompareT3Eq of m = n : compare_T3 m n false false true.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)