proposition: Lemma inj_sub x y : 0 < x < y -> Z.to_pos (y-x) = (Z.to_pos y - Z.to_pos x)%positive.
proof: Proof. destruct x; try easy. destruct y; try easy. simpl. intros. now rewrite Z.pos_sub_gt. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass