proposition: Lemma l13_6_bis : forall lp l1 l2 a, Lcos lp l1 a -> Lcos lp l2 a -> EqL l1 l2.
proof: Proof. intros. induction(is_null_anga_dec a). apply lcos_lg_anga in H. apply lcos_lg_anga in H0. spliter. assert(HH:= null_lcos_eql lp l1 a H H1). assert(HP:= null_lcos_eql lp l2 a H0 H1). transitivity lp; auto. symmetry; auto. apply lcos_lg_anga in H. apply lcos_lg_anga in H0. spliter. assert (HH:= H). assert(HH0:= H0). unfold Lcos in HH. unfold Lcos in HH0. spliter. ex_and H11 A. ex_and H16 B. ex_and H11 C. ex_and H15 A'. ex_and H19 B'. ex_and H15 C'. assert(HH:=not_null_not_col a B A C H4 H1 H18). assert(HP:=not_null_not_col a B' A' C' H4 H1 H21). assert(B <> C). intro. subst C. apply HH. Col. assert(B' <> C'). intro. subst C'. apply HP. Col. assert(HQ:= anga_distincts a B A C H4 H18). assert(HR:= anga_distincts a B' A' C' H4 H21). spliter. assert(Cong A B A' B'). apply (lg_cong lp); auto. assert(CongA B A C B' A' C'). apply (anga_conga a); auto. assert(CongA C B A C' B' A'). apply l11_16; auto. assert(Cong A C A' C' /\ Cong B C B' C' /\ CongA A C B A' C' B'). apply(l11_50_1 A B C A' B' C'); auto. intro. apply HH. Col. apply conga_comm. auto. spliter. apply (all_eql A' C'). split; auto. split; auto. eapply (lg_cong_lg _ A C); auto. unfold Lcos in *;intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project