proposition: Theorem list_Q_pair_in_dec : ∀ a b (l : list (Q * Q)), {(a, b) ∈ l} + {(a, b) ∉ l}.
proof: Proof. intros a b l. apply List.In_dec. intros x y. destruct x as ((xan, xad), (xbn, xbd)). destruct y as ((yan, yad), (ybn, ybd)). destruct (Z.eq_dec xan yan) as [Han| Han]. subst xan. destruct (Pos.eq_dec xad yad) as [Had| Had]. subst xad. destruct (Z.eq_dec xbn ybn) as [Hbn| Hbn]. subst xbn. destruct (Pos.eq_dec xbd ybd) as [Hbd| Hbd]. subst xbd. left; reflexivity. right; intros H. injection H; clear H; intros; subst. apply Hbd; reflexivity. right; intros H. injection H; clear H; intros; subst. apply Hbn; reflexivity. right; intros H. injection H; clear H; intros; subst. apply Had; reflexivity. right; intros H. injection H; clear H; intros; subst. apply Han; reflexivity. Qed.
imports: Utf8 QArith Misc Field2 InSegment ConvexHull Newton NotInSegment Puiseux_base