proposition: Lemma cong2_lam2__cong_conga : forall N M P Q N' M' P' Q', Lambert N M P Q -> Lambert N' M' P' Q' -> Cong N Q N' Q' -> Cong P Q P' Q' -> Cong N M N' M' /\ CongA M P Q M' P' Q'.
proof: Proof. intros N M P Q N' M' P' Q' HLam HLam' HCong1 HCong2. assert(Par_strict N Q M P) by (apply lam__pars1423, HLam). assert(Par_strict N M P Q) by (apply lam__pars1234, HLam). assert(Par_strict N' Q' M' P') by (apply lam__pars1423, HLam'). assert(Par_strict N' M' P' Q') by (apply lam__pars1234, HLam'). unfold Lambert in *. spliter. assert(~ Col N M P) by (apply per_not_col; auto). assert(~ Col M N Q) by (apply per_not_col; auto). assert(~ Col M' N' Q') by (apply per_not_col; auto). assert_diffs. assert(HSAS := l11_49 N Q P N' Q' P'). destruct HSAS as [HCong3 [HConga1 HConga2]]; Cong; [CongA|]. assert(CongA M N P M' N' P'). { apply (l11_22b _ _ _ Q _ _ _ Q'). repeat (split; CongA); Side. } assert(HAAS := l11_50_2 P N M P' N' M'). destruct HAAS as [HCong4 [HCong5 HCong6]]; [Col|CongA..|Cong|]. split; trivial. apply (l11_22a _ _ _ N _ _ _ N'). repeat (split; Side; CongA). Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel GeoCoq.Tarski_dev.Annexes.suma