feat(data/quot): Add quotient pi induction (#11137)
I am planning to use this later to show that the (pi) product of homotopy classes of paths is well-defined, and prove
properties about that product.
Co-authored-by: prakol16 <prakol16@users.noreply.github.com>
