proposition: Lemma conga2_suppa__suppa : forall A B C D E F A' B' C' D' E' F', CongA A B C A' B' C' -> CongA D E F D' E' F' -> SuppA A B C D E F -> SuppA A' B' C' D' E' F'.
proof: Proof. intros. assert (SuppA A B C D' E' F'). { unfold SuppA in *; spliter. split; auto. ex_and H2 A0. exists A0. split; trivial. apply conga_trans with D E F; [apply conga_sym|]; assumption. } apply suppa_sym. apply suppa_sym in H2. unfold SuppA in H2; spliter. split; auto. ex_and H3 D0. exists D0. split; trivial. apply conga_trans with A B C; [apply conga_sym|]; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2