proposition: Lemma defect2__conga : forall A B C D E F D' E' F', Defect A B C D E F -> Defect A B C D' E' F' -> CongA D E F D' E' F'.
proof: Proof. intros A B C D E F D' E' F' HDef HDef'. destruct HDef as [G [H [I [HTri HSuppa]]]]. destruct HDef' as [G' [H' [I' [HTri' HSuppa']]]]. apply (suppa2__conga456 G H I); trivial. suma.assert_diffs. apply (conga2_suppa__suppa G' H' I' D' E' F'); try apply conga_refl; auto. apply (trisuma2__conga A B C); assumption. Qed.
imports: GeoCoq.Tarski_dev.Annexes.saccheri