proposition: Lemma lcos3_lcos2 : forall l1 l2 a b c d n, Eq_Lcos3 l1 a b n l2 c d n -> Eq_Lcos2 l1 a b l2 c d.
proof: Proof. intros. unfold Eq_Lcos3 in H. ex_and H lp. unfold Eq_Lcos2. apply lcos3_lcos_2_1 in H. apply lcos3_lcos_2_1 in H0. ex_and H ll1. ex_and H0 ll2. assert (EqL ll1 ll2). eapply(l13_6_bis lp _ _ n); auto. exists ll1. split; auto. apply lcos2_lg_anga in H. apply lcos2_lg_anga in H0. spliter. apply(lcos2_eql_lcos2 l2 l2 ll2 ll1 c d); auto. reflexivity. symmetry; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_4_cos GeoCoq.Tarski_dev.Annexes.project