proposition: Lemma nat_compare_consistent : forall n0 n1, { Nat.compare n0 n1 = Lt /\ Nat.compare n1 n0 = Gt } + { Nat.compare n0 n1 = Eq /\ Nat.compare n1 n0 = Eq } + { Nat.compare n0 n1 = Gt /\ Nat.compare n1 n0 = Lt }.
proof: Proof. intros n0 n1; destruct (lt_eq_lt_dec n0 n1) as [ [_lt | _eq] | _lt ]; [ constructor 1; constructor 1 | constructor 1; constructor 2 | constructor 2 ]; split; autorewrite_nat_compare; intuition. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii Coq.Structures.OrderedType Fiat.Common.Coq__8_4__8_5__Compat