proposition: Lemma sum_pos_pos : forall O E E' A B AB, Ps O E A -> Ps O E B -> Sum O E E' A B AB -> Ps O E AB.
proof: Proof. intros. unfold Ps in *. assert(Out O A B). apply l6_6 in H0. apply(l6_7 O A E B); auto. assert(HH:=l14_36_b O E E' A B AB H1 H2). spliter. assert(HH:=l14_36_a O E E' A B AB H1 H2). apply l6_6 in H. assert(Out O A AB). apply bet_out; auto. assert(HP:=l6_7 O E A AB H H6). apply l6_6. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch14_prod