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