proposition: Lemma nat_compare_elim (P : nat -> nat -> comparison -> Prop) (PEq : forall i, P i i Eq) (PLt : forall i j, i < j -> P i j Lt) (PGt : forall i j, i > j -> P i j Gt) : forall i j, P i j (Nat.compare i j).
proof: Proof. intros. case (Nat.compare_spec i j); intros; subst; auto. Qed.
imports: Equations(Equations) Lia List Utf8 Arith Lia