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