proposition: Lemma sub_iso_to U1 U2 W1 W2 tau : {subset U2 <= U1} -> {subset W1 <= W2} -> {in U1, isometry tau, to W1} -> {in U2, isometry tau, to W2}.
proof: Proof. by move=> sU sW [Itau Wtau]; split=> [|u /sU/Wtau/sW //]; apply: sub_in2 Itau. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)