proposition: Lemma compare_spec' : forall x y, match x ?= y with | Lt => x <? y | Eq => x = y | Gt => y <? x end.
proof: Proof. intros x y;rewrite compare_def_spec;unfold compare_def. case_eq (x <? y);intros;[reflexivity | ]. case_eq (x =? y);intros. rewrite <- eqb_spec;trivial. rewrite <- not_true_iff_false in H, H0. unfold is_true in *;rewrite ltb_spec in H |- *;rewrite eqb_spec in H0. assert ([|x|] <> [|y|]) by (intros Heq;apply H0, to_Z_inj;trivial);lia. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring