proposition: Lemma conga_defect__defect : forall A B C D E F D' E' F', Defect A B C D E F -> CongA D E F D' E' F' -> Defect A B C D' E' F'.
proof: Proof. intros A B C D E F D' E' F' HDef HConga. destruct HDef as [G [H [I [HTri HSuppa]]]]. exists G, H, I. split; trivial. assert_diffs. apply (conga2_suppa__suppa G H I D E F); CongA. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri