proposition: Lemma bet_cong2_grad__grad2 : forall A B C D E F, Grad A B C -> Bet D E F -> Cong A B D E -> Cong B C E F -> Grad2 A B C D E F.
proof: Proof. intros A B C D E F HGrad. destruct (eq_dec_points D E). { intros; treat_equalities. apply grad112__eq in HGrad. treat_equalities; apply grad2_init. } revert F. induction HGrad. intros; treat_equalities; apply grad2_init. intros F' HBet HCong1 HCong2. destruct (segment_construction D E B C) as [F []]. destruct (eq_dec_points E F). treat_equalities; apply grad2_stab with B E; trivial; [apply grad2_init|CongR]. assert (Bet B C C'). apply grad__bet in HGrad; apply between_exchange3 with A; assumption. assert (Bet E F F'). { apply cong_preserves_bet with B C C'; Cong. assert_diffs. apply l6_2 with D; Between. } apply grad2_stab with C F; Cong. apply outer_transitivity_between2 with E; trivial. apply cong_transitivity with A B; Cong. apply cong_transitivity with C C'; trivial. apply l4_3_1 with B E; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations