proposition: Lemma eq_complete : forall x, eq x x = true.
proof: Proof. intros [[l | |][u| |]]; simpl; auto; try case (Z.eq_dec l l); try case (Z.eq_dec u u); intros; auto; try match goal with id :~_ |- _ => case id; apply refl_equal end. Qed.
imports: ZArith List Lia