proposition: Lemma Exercise1_22p x: open_r r x -> x = (open_bar r x) .
proof: Proof. move=> [osr p3];move: (Exercise1_22g osr) (Exercise1_22i osr). by move=> p1 [p2a p2b]; apply: (p3 _ p2a p1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)