proposition: Lemma anga_out_anga : forall a A B C A' C', Q_CongA_Acute a -> a A B C -> Out B A A' -> Out B C C' -> a A' B C'.
proof: Proof. intros. assert(HH:= H). unfold Q_CongA_Acute in HH. ex_and HH A0. ex_and H3 B0. ex_and H4 C0. assert(HP:= H4 A B C). destruct HP. assert(CongA A0 B0 C0 A B C). apply H6. auto. assert(HP:= anga_distincts a A B C H H0). spliter. assert(CongA A B C A' B C'). apply out2__conga; apply l6_6; assumption. assert(HH:= H4 A' B C'). destruct HH. apply H11. apply (conga_trans _ _ _ A B C); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length Setoid