proposition: Lemma gradexpinv_clos_trans : forall A B C, GradExpInv A B C <-> clos_refl_trans_1n Tpoint (fun X Y => Midpoint X A Y) B C.
proof: Proof. intros; split; induction 1; try constructor. apply Relation_Operators.rt1n_trans with B; [split|]; assumption. apply gradexpinv_stab with y; Between; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations