proposition: Theorem non_trivial_realizer : forall e, non_trivial↓e ⊩ (0 << 1)%Re.
proof: Proof. intro e. start. apply Qq_realizer. eexists (_ → _ → _). find; repeat (start; apply Qq_realizer; find); [Ksolve |..]; find; try apply prop_realizer1; now split || compute. Qed.
imports: ClassicalRealizability.Kbase ClassicalRealizability.Rationals ClassicalRealizability.Real_definitions ClassicalRealizability.Real_relations ClassicalRealizability.Real_operations