proposition: Lemma gradexp__gradexpinv : forall A B C, GradExp A B C <-> GradExpInv A B C.
proof: Proof. intros. rewrite gradexp_clos_trans, gradexpinv_clos_trans. rewrite <- clos_rt_rt1n_iff, <- clos_rt_rtn1_iff. reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality Relations