proposition: Lemma prop_32_2 : forall A B C D, A <> B -> B <> C -> A <> C -> Bet B C D -> C <> D -> SumA C A B A B C A C D.
proof: Proof. intros A B C D HAB HBC HAC HBet HAD. destruct (ex_trisuma C A B) as [P [Q [R HTri]]]; auto. assert (Bet P Q R) by (apply (prop_32_1 C A B), HTri). destruct HTri as [S [T [U [HSuma1 HSumA2]]]]. apply conga3_suma__suma with C A B A B C S T U; try (apply conga_refl); auto. assert_diffs. assert (HCongA : CongA B C D P Q R) by (apply conga_line; auto). assert (HSumA' : SumA A C D B C A P Q R). apply conga3_suma__suma with A C D B C A B C D; CongA. apply suma_sym, bet__suma; auto. apply sams2_suma2__conga123 with B C A P Q R; trivial; apply bet_suma__sams with P Q R; assumption. Qed.
imports: GeoCoq.Meta_theory.Continuity.elementary_continuity_props GeoCoq.Tarski_dev.Ch16_coordinates_with_functions