proposition: Lemma length_Ps : forall O E E' A B AB, AB <> O -> Length O E E' A B AB -> Ps O E AB.
proof: Proof. intros. unfold Length in H0. spliter. unfold LeP in H2. induction H2. unfold LtP in H2. ex_and H2 X. apply diff_sum in H2. apply sum_cong in H2. unfold Parallelogram_flat in H2. spliter. apply cong_symmetry in H6. apply cong_identity in H6. subst X. assumption. unfold Sum in H2. spliter. unfold Ar2 in H2. tauto. right. intro. subst X. unfold Ps in H4. unfold Out in H4. tauto. subst AB. tauto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order