proposition: Lemma suppa2__conga123 : forall A B C D E F A' B' C', SuppA A B C D E F -> SuppA A' B' C' D E F -> CongA A B C A' B' C'.
proof: Proof. intros. apply (suppa2__conga456 D E F); apply suppa_sym; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2