proposition: Lemma compare_reflect : forall a b, match compare a b with | Datatypes.Lt => lt a b | Eq => a = b | Gt => lt b a end.
proof: Proof. unfold lt; induction a as [ | [p n]]. - destruct b. + easy. + cbn; now destruct p. - destruct b as [ | [p0 n0] b]. + cbn; trivial. + cbn; specialize (IHa b); rewrite compare_rev with a b; rewrite Nat.compare_antisym in * ; destruct (compare a b), (p0 ?= p) eqn:Heq; simpl in *; subst; try easy; apply Nat.compare_eq_iff in Heq as -> ; destruct (n ?= n0) eqn:Heqc; trivial. * destruct (compare _ _) eqn: H. apply Nat.compare_eq_iff in Heqc as ->. rewrite IHa. reflexivity. reflexivity. rewrite Nat.compare_antisym. rewrite Heqc. reflexivity. * destruct (n ?= n0) eqn:Heqn; trivial; now rewrite Nat.compare_antisym, Heqn. * destruct (compare _ _) eqn: H. apply Nat.compare_eq_iff in Heqc as ->. rewrite IHa. reflexivity. reflexivity. rewrite Nat.compare_antisym. rewrite Heqc. reflexivity. * destruct (n ?= n0) eqn:?; trivial; try discriminate. rewrite Nat.compare_antisym; now rewrite Heqc0. * destruct (compare _ _) eqn: H. apply Nat.compare_eq_iff in Heqc as ->. rewrite IHa. reflexivity. reflexivity. rewrite Nat.compare_antisym. rewrite Heqc. reflexivity. * rewrite Nat.compare_antisym. rewrite Heqc. reflexivity. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )