proposition: Lemma compare_correct {n} (alpha beta : t n) : CompSpec eq lt alpha beta (compare alpha beta).
proof: Proof. destruct n. - assert False by (now apply t0_empty); contradiction. - destruct alpha, beta; cbn; case_eq (x ?= x0); unfold lt; cbn. + rewrite Nat.compare_eq_iff; intro; subst; f_equal. constructor 1. f_equal. apply eq_proofs_unicity_on; decide equality. + rewrite Nat.compare_lt_iff; constructor 2. simpl; destruct x0; [ lia | apply leb_correct; lia]. + rewrite Nat.compare_gt_iff; constructor 3. simpl; destruct x; [lia | apply leb_correct; lia]. Qed.
imports: Coq(Arith Relations Lia Logic.Eqdep_dec Ensembles Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses) hydras(ON_Generic)