proposition: Lemma sub_diag p : p-p = 1.
proof: Proof. unfold sub. now rewrite sub_mask_diag. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef