proposition: Lemma norm_aux_PEopp pe : match get_PEopp pe with | Some pe' => norm_aux pe = -- (norm_aux pe') | None => True end.
proof: Proof. now destruct pe. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory