proposition: Lemma trichoP (a b: U) : CompareSpec (a == b) (a < b)%O (b < a)%O (tricho a b).
proof: Proof. rewrite /tricho; case Hab: (a == b) => //; [by constructor|]. case H'ab: (a < b)%O; constructor => //. rewrite Order.POrderTheory.lt_def; apply /andP; split. - by rewrite /negb Hab. - have diff : a != b by rewrite Hab . move: diff; rewrite Order.TotalTheory.neq_lt H'ab Bool.orb_false_l; by apply: Order.POrderTheory.ltW. Qed.
imports: mathcomp(all_ssreflect zify) mathcomp(fintype) Coq(Logic.Eqdep_dec) Coq(Wellfounded.Inclusion Wf_nat Inverse_Image)