proposition: Theorem add_sub_eq2 : forall a b c : Qpositive, a <> b -> Qpositive_le b a -> c = Qpositive_sub a b -> Qpositive_plus b c = a.
proof: Proof. intros a b c H H0 H1; rewrite H1; rewrite Qpositive_plus_sym; rewrite Qpositive_sub_correct2; auto with *. Qed.