fact: Definition tricho (a b: U) := if (a == b)%O then Eq else if (a < b)%O then Lt else Gt.
imports: mathcomp(all_ssreflect zify) mathcomp(fintype) Coq(Logic.Eqdep_dec) Coq(Wellfounded.Inclusion Wf_nat Inverse_Image)