proposition: Lemma finord_compare_correct (n:nat) (alpha beta : 'I_n) : CompSpec eq (@finord_lt n) alpha beta (compare alpha beta).
proof: Proof. case (PeanoNat.Nat.compare_spec alpha beta) => H. - move : H; rewrite /nat_of_ord /compare. destruct alpha, beta => ?; subst. have Heq:i = i0. + apply eq_proofs_unicity_on. decide equality. + subst; rewrite /finord_compare PeanoNat.Nat.compare_refl. by constructor. - replace (compare alpha beta) with Datatypes.Lt. + constructor; rewrite /finord_lt; by apply /ltP. + symmetry; by rewrite /compare PeanoNat.Nat.compare_lt_iff. - replace (compare alpha beta) with Datatypes.Gt. + constructor; rewrite /finord_lt; by apply /ltP. + symmetry; by rewrite /compare PeanoNat.Nat.compare_gt_iff. Qed.
imports: hydras(DecPreOrder ON_Generic) mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec)