proposition: Theorem Qpositive_c_unfold1 : forall p q n : nat, S p + S q + S q <= S n -> Qpositive_c (S p + S q) (S q) (S n) = nR (Qpositive_c (S p) (S q) n).
proof: Proof. intros p q n Hle; simpl in |- *. rewrite <- (plus_n_Sm p q). rewrite Nat.sub_succ_l. rewrite Nat.add_sub; auto with *. auto with arith. Qed.