proposition: Lemma Exercise6_32_sym A B k0: Exercise6_32_conc A B k0 -> Exercise6_32_conc B A k0.
proof: Proof. move => [f [fa fb fc]]. move: (inverse_bij_bp fa) => fai. exists (inverse_fun f); split => // i k iz kp. move:(fb i k iz kp) =>[j ja jb]; exists j => //. by rewrite (ifun_involutive (proj1 (proj1 (proj31 fa)))). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)