proposition: Lemma root_uniqueness : forall O E E' A B C, ~Ng O E A -> ~Ng O E B -> Prod O E E' A A C -> Prod O E E' B B C -> A = B.
proof: Proof. intros O E E' A B C PA PB. intros. assert(~ Col O E E' /\ Col O E A /\ Col O E B /\ Col O E C). { unfold Prod in *. unfold Ar2 in *. tauto. } spliter. assert(HS:= sum_exists O E E' H1 A B H2 H3). ex_and HS ApB. assert(HD:= diff_exists O E E' A B H1 H2 H3). ex_and HD AmB. assert(Col O E ApB /\ Col O E AmB). { unfold Sum in H5. unfold Diff in H6. ex_and H6 X. unfold Sum in H7. unfold Ar2 in *. tauto. } spliter. assert(HP:= prod_exists O E E' H1 ApB AmB H7 H8). ex_and HP PP. assert(Diff O E E' C C O). { apply diff_null; auto. } assert(HH:= diff_of_squares O E E' A B C C O ApB AmB PP H H0 H10 H5 H6 H9). treat_equalities. assert(HH:= prod_null O E E' ApB AmB H9). induction (eq_dec_points A O). { subst A. apply prod_O_l_eq in H. subst C. apply prod_null in H0. induction H0; subst B; auto. } { assert(E <> O). { intro. subst E; Col. } induction (eq_dec_points B O). { subst B. apply prod_O_l_eq in H0. subst C. apply prod_null in H. induction H; subst A; auto. } { induction HH. { assert(Ps O E A \/ A = O). { apply(not_neg_pos O E A); auto. } assert(Ps O E B \/ B = O). { apply(not_neg_pos O E B); auto. } induction H15; induction H16; try(contradiction). { assert(HP:=sum_pos_pos O E E' A B ApB H15 H16 H5). unfold Ps in HP. unfold Out in HP. subst ApB. tauto. } } { subst AmB. apply diff_null_eq in H6. auto. } } } Qed.
imports: GeoCoq.Tarski_dev.Ch14_order