proposition: Lemma conga2_grada__grada : forall A B C D E F A' B' C' D' E' F', GradA A B C D E F -> CongA A B C A' B' C' -> CongA D E F D' E' F' -> GradA A' B' C' D' E' F'.
proof: Proof. intros A B C D E F A' B' C' D' E' F' HGA. revert A' B' C' D' E' F'. induction HGA; intros A' B' C' D' E' F' Hconga1 Hconga2. apply grada_init, conga_trans with D E F; trivial; apply conga_trans with A B C; CongA. suma.assert_diffs. assert (Hconga3 : CongA D E F D E F) by CongA. apply grada_stab with D E F. apply (IHHGA A' B' C' D E F); trivial. apply (conga2_sams__sams D E F A B C); trivial. apply (conga3_suma__suma D E F A B C G H I); trivial. Qed.
imports: GeoCoq.Axioms.continuity_axioms GeoCoq.Meta_theory.Continuity.archimedes GeoCoq.Tarski_dev.Annexes.suma GeoCoq.Tarski_dev.Ch12_parallel