fact: CoInductive tuto_compare_nat (m n : nat) : bool -> bool -> bool -> Set := | TCompareNatLt of m < n : tuto_compare_nat m n true false false | TCompareNatGt of m > n : tuto_compare_nat m n false true false | TCompareNatEq of m = n : tuto_compare_nat m n false false true.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset)