Section ser. Let false:=False. Let false_ind:=False_ind. Variable dom:Set. Variable goal:Prop. Variable less:dom->dom->Prop. Variable p:dom->Prop. Variable o:dom. Hypothesis left_to_right:forall A B:dom,(p A)/\(less A B)/\(p B)->false. Hypothesis right_to_left:forall A:dom,(p A) \/ (exists B:dom,(less A B)/\(p B)). Hypothesis transitive_less:forall A B C:dom,(less A B)/\(less B C)->(less A C). Hypothesis serial_less:forall A:dom,(exists B:dom,(less A B)). Lemma ser1: (p o) \/ (exists A:dom,(less o A)/\(p A)). Proof. exact ((right_to_left o)). Qed. Lemma ser2: (p o)->(exists A:dom,(less o A)). Proof. exact (fun (Vpo:(p o))=>(serial_less o)). Qed. Lemma ser3: (p o)->forall C0:dom,(less o C0)->(p C0) \/ (exists A:dom,(less C0 A)/\(p A)). Proof. exact (fun (Vpo:(p o))(C0:dom)(VlessoC0:(less o C0))=>(right_to_left C0)). Qed. Lemma ser4: (p o)->forall C0:dom,(less o C0)->(p C0)->false. Proof. exact (fun (Vpo:(p o))(C0:dom)(VlessoC0:(less o C0))(VpC0:(p C0))=>((left_to_right o C0) (conj Vpo (conj VlessoC0 VpC0)))). Qed. Lemma ser5: (p o)->forall C0:dom,(less o C0)->(p C0)->goal. Proof. exact (fun (Vpo:(p o))(C0:dom)(VlessoC0:(less o C0))(VpC0:(p C0))=>((false_ind goal) (ser4 Vpo C0 VlessoC0 VpC0))). Qed. Lemma ser6: (p o)->forall C0:dom,(less o C0)->forall C1:dom,(less C0 C1)->(p C1)->(less o C1). Proof. exact (fun (Vpo:(p o))(C0:dom)(VlessoC0:(less o C0))(C1:dom)(VlessC0C1:(less C0 C1))(VpC1:(p C1))=>((transitive_less o C0 C1) (conj VlessoC0 VlessC0C1))). Qed. Lemma ser7: (p o)->forall C0:dom,(less o C0)->forall C1:dom,(less C0 C1)->(p C1)->false. Proof. exact (fun (Vpo:(p o))(C0:dom)(VlessoC0:(less o C0))(C1:dom)(VlessC0C1:(less C0 C1))(VpC1:(p C1))=>((left_to_right o C1) (conj Vpo (conj (ser6 Vpo C0 VlessoC0 C1 VlessC0C1 VpC1) VpC1)))). Qed. Lemma ser8: (p o)->forall C0:dom,(less o C0)->forall C1:dom,(less C0 C1)->(p C1)->goal. Proof. exact (fun (Vpo:(p o))(C0:dom)(VlessoC0:(less o C0))(C1:dom)(VlessC0C1:(less C0 C1))(VpC1:(p C1))=>((false_ind goal) (ser7 Vpo C0 VlessoC0 C1 VlessC0C1 VpC1))). Qed. Lemma ser9: (p o)->forall C0:dom,(less o C0)->goal. Proof. exact (fun (Vpo:(p o))(C0:dom)(VlessoC0:(less o C0))=>((or_ind ((ser5 Vpo C0 VlessoC0))(ex_ind (P:=fun C1:dom=>(less C0 C1)/\(p C1))(fun C1:dom=>(and_ind (ser8 Vpo C0 VlessoC0 C1)))))(ser3 Vpo C0 VlessoC0))). Qed. Lemma ser10: (p o)->goal. Proof. exact (fun (Vpo:(p o))=>((ex_ind (P:=fun C0:dom=>(less o C0))(fun C0:dom=>((ser9 Vpo C0))))(ser2 Vpo))). Qed. Lemma ser11: forall C0:dom,(less o C0)->(p C0)->(exists A:dom,(less C0 A)). Proof. exact (fun (C0:dom)(VlessoC0:(less o C0))(VpC0:(p C0))=>(serial_less C0)). Qed. Lemma ser12: forall C0:dom,(less o C0)->(p C0)->forall C1:dom,(less C0 C1)->(p C1) \/ (exists A:dom,(less C1 A)/\(p A)). Proof. exact (fun (C0:dom)(VlessoC0:(less o C0))(VpC0:(p C0))(C1:dom)(VlessC0C1:(less C0 C1))=>(right_to_left C1)). Qed. Lemma ser13: forall C0:dom,(less o C0)->(p C0)->forall C1:dom,(less C0 C1)->(p C1)->false. Proof. exact (fun (C0:dom)(VlessoC0:(less o C0))(VpC0:(p C0))(C1:dom)(VlessC0C1:(less C0 C1))(VpC1:(p C1))=>((left_to_right C0 C1) (conj VpC0 (conj VlessC0C1 VpC1)))). Qed. Lemma ser14: forall C0:dom,(less o C0)->(p C0)->forall C1:dom,(less C0 C1)->(p C1)->goal. Proof. exact (fun (C0:dom)(VlessoC0:(less o C0))(VpC0:(p C0))(C1:dom)(VlessC0C1:(less C0 C1))(VpC1:(p C1))=>((false_ind goal) (ser13 C0 VlessoC0 VpC0 C1 VlessC0C1 VpC1))). Qed. Lemma ser16: forall C0:dom,(less o C0)->(p C0)->forall C1:dom,(less C0 C1)->forall C2:dom,(less C1 C2)->(p C2)->(less C0 C2). Proof. exact (fun (C0:dom)(VlessoC0:(less o C0))(VpC0:(p C0))(C1:dom)(VlessC0C1:(less C0 C1))(C2:dom)(VlessC1C2:(less C1 C2))(VpC2:(p C2))=>((transitive_less C0 C1 C2) (conj VlessC0C1 VlessC1C2))). Qed. Lemma ser17: forall C0:dom,(less o C0)->(p C0)->forall C1:dom,(less C0 C1)->forall C2:dom,(less C1 C2)->(p C2)->false. Proof. exact (fun (C0:dom)(VlessoC0:(less o C0))(VpC0:(p C0))(C1:dom)(VlessC0C1:(less C0 C1))(C2:dom)(VlessC1C2:(less C1 C2))(VpC2:(p C2))=>((left_to_right C0 C2) (conj VpC0 (conj (ser16 C0 VlessoC0 VpC0 C1 VlessC0C1 C2 VlessC1C2 VpC2) VpC2)))). Qed. Lemma ser18: forall C0:dom,(less o C0)->(p C0)->forall C1:dom,(less C0 C1)->forall C2:dom,(less C1 C2)->(p C2)->goal. Proof. exact (fun (C0:dom)(VlessoC0:(less o C0))(VpC0:(p C0))(C1:dom)(VlessC0C1:(less C0 C1))(C2:dom)(VlessC1C2:(less C1 C2))(VpC2:(p C2))=>((false_ind goal) (ser17 C0 VlessoC0 VpC0 C1 VlessC0C1 C2 VlessC1C2 VpC2))). Qed. Lemma ser19: forall C0:dom,(less o C0)->(p C0)->forall C1:dom,(less C0 C1)->goal. Proof. exact (fun (C0:dom)(VlessoC0:(less o C0))(VpC0:(p C0))(C1:dom)(VlessC0C1:(less C0 C1))=>((or_ind ((ser14 C0 VlessoC0 VpC0 C1 VlessC0C1))(ex_ind (P:=fun C2:dom=>(less C1 C2)/\(p C2))(fun C2:dom=>(and_ind (ser18 C0 VlessoC0 VpC0 C1 VlessC0C1 C2)))))(ser12 C0 VlessoC0 VpC0 C1 VlessC0C1))). Qed. Lemma ser20: forall C0:dom,(less o C0)->(p C0)->goal. Proof. exact (fun (C0:dom)(VlessoC0:(less o C0))(VpC0:(p C0))=>((ex_ind (P:=fun C1:dom=>(less C0 C1))(fun C1:dom=>((ser19 C0 VlessoC0 VpC0 C1))))(ser11 C0 VlessoC0 VpC0))). Qed. Lemma ser21: goal. Proof. exact (((or_ind (ser10)(ex_ind (P:=fun C0:dom=>(less o C0)/\(p C0))(fun C0:dom=>(and_ind (ser20 C0)))))ser1)). Qed. Check ser21. End ser.