feat: Add DropPair ProdP commutation lemma for one orientation - #1345

Open

NicolaBernini wants to merge 8 commits into

leanprover-community:masterfrom

NicolaBernini:feat/add-DropPair-ProdP-commutation-lemmas-for-one-orientation-1July2026

Commits on Jul 1, 2026

Commits on Jul 3, 2026

fix: make succSuccAbove cast lengths explicit

NicolaBernini
and
Claude Opus 4.8
committed
fix: require distinct indices for castAdd drop-pair lemmas

NicolaBernini
and
Claude Opus 4.8
committed
fix: make append castAdd reindexing use identity

NicolaBernini
and
Claude Opus 4.8
committed
fix: drop fragile left-factor dropPair commutation

NicolaBernini
and
Claude Opus 4.8
committed