proposition: Lemma psos_r1: forall x y, x == y -> x - y == 0.
proof: Proof. intros x y H; simpl; setoid_rewrite H; simpl; cring. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia