proposition: Lemma sum_cong : forall A B C, Sum O E E' A B C -> (A <> O \/ B <> O) -> Parallelogram_flat O A C B.
proof: Proof. intros. induction(eq_dec_points A O). subst A. assert(HP:= (sum_O_B_eq B C H)). subst C. induction H0. tauto. assert(Parallelogram O O B B). apply plg_trivial1; auto. induction H1. apply False_ind. unfold Parallelogram_strict in H1. spliter. apply par_distincts in H2. tauto. assumption. assert(exists A' C' : Tpoint, Plg O B C' A' /\ Plg C' A' A C). apply(sum_plg A B C); auto. ex_and H2 A'. ex_and H3 C'. apply plg_to_parallelogram in H2. apply plg_to_parallelogram in H3. apply plgf_permut. assert(HH:=plg_pseudo_trans O B C' A' A C H2 H3). induction HH. induction H4. apply False_ind. apply H4. unfold Sum in H. spliter. unfold Ar2 in H. spliter. assert_diffs. ColR. apply plgf_comm2. auto. spliter. subst A. apply False_ind. subst C. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_6_Desargues_Hessenberg