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