proposition: Theorem Qpositive_le_trans : forall w w' w'' : Qpositive, Qpositive_le w w' -> Qpositive_le w' w'' -> Qpositive_le w w''.
proof: Proof. intros w w'; generalize w; elim w'; unfold Qpositive_le in |- *; simpl in |- *; clear w w'. intros w' Hrec w; case w. 3: intros w''; case w''; simpl in |- *; auto. intros w0 w''; case w''; simpl in |- *; auto. intros w0 w''; case w''; simpl in |- *; auto. intros w''0 H H1; discriminate H1. intros w' Hrec w; case w. 3: intros w'' H; discriminate H. intros w0 w'' H; discriminate H. intros w0 w''; case w''; simpl in |- *; auto. intros w; case w; clear w; simpl in |- *. 3: auto. intros w w'' H; discriminate H. intros w w''; case w''; simpl in |- *; auto. intros w''0 H H1; discriminate H1. Qed.