proposition: Lemma conga_bet_conga : forall A B C D E F A' C' D' F', CongA A B C D E F -> A' <> B -> C' <> B -> D' <> E -> F' <> E -> Bet A B A' -> Bet C B C' -> Bet D E D' -> Bet F E F' -> CongA A' B C' D' E F'.
proof: Proof. intros. assert(HH:= l11_13 A B C D E F A' D' H H4 H0 H6 H2). apply conga_comm. apply(l11_13 C B A' F E D' C' F'); auto. apply conga_comm. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order