proposition: Lemma in_angle_asym : forall A B C D, InAngle D A B C -> InAngle C A B D -> CongA A B C A B D.
proof: Proof. intros. unfold InAngle in *. spliter. ex_and H3 CC. ex_and H6 DD. induction H7; induction H8. subst DD. subst CC. apply conga_line; try assumption. auto. auto. subst CC. unfold Out in H8. spliter. induction H9. assert(Bet A B C). apply between_exchange4 with DD; trivial. eapply between_inner_transitivity. apply H3. assumption. apply conga_line; try assumption. auto. auto. assert(Bet A B C). eapply between_exchange4. eapply outer_transitivity_between. apply H3. apply H9. auto. assumption. apply conga_line; try assumption. auto. auto. subst DD. assert(Bet A B D). unfold Out in H7. spliter. induction H9. eapply between_exchange4. eapply between_inner_transitivity. apply H6. apply H9. assumption. eapply between_exchange4. eapply outer_transitivity_between. apply H6. apply H9. auto. assumption. apply conga_line; try assumption. auto. auto. assert(exists B', Bet CC B' C /\ Bet DD B' D). eapply inner_pasch. apply between_symmetry. apply H3. apply between_symmetry. assumption. ex_and H9 X. assert (Out B X C). eapply out_bet_out_2. apply H7. assumption. assert(Out B X D). eapply out_bet_out_2. apply H8. assumption. assert (Out B C D). apply l6_7 with X. apply l6_6. assumption. assumption. apply out2__conga. apply out_trivial. auto. apply l6_6. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2