proposition: Lemma ge_is_rclosure_gt : forall `{Le A}, refl le -> ge = rclosure gt.
proof: Proof. Proof using. intros. rewrite gt_is_strict_ge. rewrite~ rclosure_strict. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOperation LibRelation)