proposition: Lemma path_to a g z p : path (relto a g) z p = (path g z p) && (all a p).
proof: Proof. apply/(pathP z)/idP => [fgi|/andP[/pathP gi] /allP ga]; last first. by move=> i i_lt /=; rewrite gi ?andbT ?[_ \in _]ga // mem_nth. rewrite (appP (pathP z) idP) //=; last by move=> i /fgi /= /andP[_ ->]. by apply/(all_nthP z) => i /fgi /andP []. Qed.
imports: HB(structures) mathcomp(all_ssreflect)